Push API: move PushManager from Navigator to ServiceWorkerRegistration [switchover 6/6]

Source/modules/push_messaging/ServiceWorkerRegistrationPush.idl

Index: Source/modules/push_messaging/ServiceWorkerRegistrationPush.idl
diff --git a/Source/modules/push_messaging/ServiceWorkerRegistrationPush.idl b/Source/modules/push_messaging/ServiceWorkerRegistrationPush.idl
new file mode 100644
index 0000000000000000000000000000000000000000..d999721e1bb732a20973a14c31a5d490a0aec899
--- /dev/null
+++ b/Source/modules/push_messaging/ServiceWorkerRegistrationPush.idl
@@ -0,0 +1,12 @@
+// Copyright 2014 The Chromium Authors. All rights reserved.
+// Use of this source code is governed by a BSD-style license that can be
+// found in the LICENSE file.
+
+// http://www.w3.org/TR/push-api/#extensions-to-the-serviceworkerregistration-interface
+
+[
+    RuntimeEnabled=PushMessaging,
+] partial interface ServiceWorkerRegistration {
+    // FIXME: this may be renamed depending on the result of https://github.com/w3c/push-api/issues/47

[Peter Beverloo, 2014/12/10 00:18:18]

This FIXME feels a bit useless. If we rename it we'll send a patch, if we
don't... we don't have to send a patch. Not we have to send a patch for either
outcome.

[Michael van Ouwerkerk, 2014/12/10 15:13:06]

You asked for a TODO here. Are you sure about this? I'm not sure I understand
what you're looking for here. Either way, it's trivial, but I'd prefer not to
have such a comment as the consensus seems to be to use pushManager of type
PushManager.

+    readonly attribute PushManager pushManager;
+};