Editorial: define and export 'push' permission (#344)

Author: marcoscaceres

index.html

@@ -303,7 +303,8 @@ <h2>
           Permission
         </h2>
         <p>
-          The Push API is a [=powerful feature=], requiring [=express permission=] to be used.
+          The Push API is a [=powerful feature=] identified by the [=powerful feature/name=]
+          <dfn class="permission export">"push"</dfn>.
         </p>
         <p>
           For integration with the [[[Permissions]]] specification, this specification defines the