Refresh web page when instanceId changed

gitpod-io · Apr 3, 2022 · e353cd1 · e353cd1
1 parent f8e204b
commit e353cd1
Showing 1 changed file with 12 additions and 1 deletion.
diff --git a/components/supervisor/frontend/src/index.ts b/components/supervisor/frontend/src/index.ts
@@ -108,9 +108,20 @@ const toStop = new DisposableCollection();
     //#region current-frame
     let current: HTMLElement = loading.frame;
     let desktopRedirected = false;
+    let currentInstanceId = "";
     const nextFrame = () => {
         const instance = gitpodServiceClient.info.latestInstance;
         if (instance) {
+            // refresh web page when instanceId changed
+            if (currentInstanceId !== "") {
+                if (instance.id !== currentInstanceId && instance.ideUrl !== "") {
+                    currentInstanceId = instance.id;
+                    window.location.href = instance.ideUrl;
+                    return;
+                }
+            } else {
+                currentInstanceId = instance.id;
+            }
             if (instance.status.phase === 'running') {
                 if (!hideDesktopIde) {
                     if (isDesktopIde == undefined) {
@@ -148,7 +159,7 @@ const toStop = new DisposableCollection();
     }
     const updateCurrentFrame = () => {
         const newCurrent = nextFrame();
-        if (current === newCurrent) {
+        if (newCurrent == null || current === newCurrent) {
             return;
         }
         current.style.visibility = 'hidden';