w3c/push-api — pull request #19 by mvano (2014-08-27 14:16:52+00:00)
Title: Rename PushManager to PushRegistrationManager

* Rename PushManager to PushRegistrationManager
* Rename navigator.push to navigator.pushRegistrationManager

As discussed previously here:
http://lists.w3.org/Archives/Public/public-webapps/2014AprJun/0223.html