From f30bf3d5fff905421ee4f5e91452c02a6355407d Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 8 Jul 2024 17:28:50 +0200 Subject: [PATCH] Meta: tidy up formatting --- index.html | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/index.html b/index.html index c6423e8..4661dc1 100644 --- a/index.html +++ b/index.html @@ -115,10 +115,10 @@

Push messaging is best suited to occasions where there is not already an active communications channel established between the user agent and the web application. Sending push messages requires considerably more resources when compared with more - direct methods of communication such as the [[Fetch|Fetch API]] or [[WebSockets]]. - Push messages usually have higher latency than direct communications and they can - also be subject to restrictions on use. Most push services limit the size and - quantity of push messages that can be sent. + direct methods of communication such as the [[Fetch|Fetch API]] or [[WebSockets]]. Push + messages usually have higher latency than direct communications and they can also be + subject to restrictions on use. Most push services limit the size and quantity of + push messages that can be sent.

@@ -229,8 +229,8 @@

  • When the push subscription request has completed successfully:
      -
    1. Set |subscription|'s {{PushSubscription/endpoint}} attribute to the - push subscription's push endpoint. +
    2. Set |subscription|'s {{PushSubscription/endpoint}} attribute to the push + subscription's push endpoint.
    3. If provided by the push subscription, set |subscription|'s {{PushSubscription/expirationTime}}.