[w3c/push-api] Editorial: allOptions (#281)

> Let allOptions be the value of the options argument, if provided, or a PushSubscriptionOptions dictionary with default values. 

This isn't really needed. By the time your algorithm runs this is already done. So you should just refer to _options_ directly.

-- 
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub:
https://github.com/w3c/push-api/issues/281