fix gitpod-io#3797: [code] reconnect to the extension host

trilogy-group · Apr 8, 2021 · cb894a0 · cb894a0
1 parent d2e50e5
commit cb894a0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/components/ide/code/leeway.Dockerfile b/components/ide/code/leeway.Dockerfile
@@ -30,7 +30,7 @@ RUN sudo apt-get update \
     && sudo apt-get clean -y \
     && rm -rf /var/lib/apt/lists/*
 
-ENV GP_CODE_COMMIT a752a8a6ceb43b9add71c7d68f56b0acbdd5dcb7
+ENV GP_CODE_COMMIT e3ac4478d45fb75589b8fe975ddba55ca1559948
 RUN mkdir gp-code \
     && cd gp-code \
     && git init \

diff --git a/components/supervisor/frontend/src/ide/ide-web-socket.ts b/components/supervisor/frontend/src/ide/ide-web-socket.ts
@@ -34,6 +34,11 @@ class IDEWebSocket extends ReconnectingWebSocket {
             this.reconnect();
         }
     }
+    static disconnectWorkspace(): void {
+        for (const socket of workspaceSockets) {
+            socket.close();
+        }
+    }
 }
 
 export function install(): void {