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
+    readonly attribute PushManager pushManager;
+};