WebSocket Pepper API: make the API out of dev

ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc

Index: ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc
diff --git a/ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc b/ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc
index 284e56d6b16505754ee0b740bb41a6755b6aa57d..9eb4215bd8086853948e93ea297c881104e1bb14 100644
--- a/ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc
+++ b/ppapi/native_client/src/shared/ppapi_proxy/browser_globals.cc
@@ -416,10 +416,10 @@ const PPB_View* PPBViewInterface() {
   return ppb;
 }
 
-const PPB_WebSocket_Dev* PPBWebSocketInterface() {
-  static const PPB_WebSocket_Dev* ppb =
-      static_cast<const PPB_WebSocket_Dev*>(
-          GetBrowserInterfaceSafe(PPB_WEBSOCKET_DEV_INTERFACE));
+const PPB_WebSocket* PPBWebSocketInterface() {
+  static const PPB_WebSocket* ppb =
+      static_cast<const PPB_WebSocket*>(
+          GetBrowserInterfaceSafe(PPB_WEBSOCKET_INTERFACE));
   return ppb;
 }