fix(WebSocketClient): change port number to fit local setup and chang…

…e it when using the github action
SoftVarE-Group · Nov 3, 2023 · 038a3ad · 038a3ad
1 parent 1769081
commit 038a3ad
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/.github/workflows/playground_deployment.yml b/.github/workflows/playground_deployment.yml
@@ -31,6 +31,8 @@ jobs:
       - name: Set hostname for WebSocketLanguageServer
         run: |
           sed -i "s/languageServerHostName: .*/languageServerHostName: \"$HOSTNAME\",/" ./WebSocketClient/UVLPlayground/src/config.ts
+          sed -i "s/port: .*/port: 8010,/" ./WebSocketClient/UVLPlayground/src/config.ts
+
       - name: Build
         working-directory: WebSocketClient/UVLPlayground
         run: npm run build

diff --git a/WebSocketClient/UVLPlayground/src/config.ts b/WebSocketClient/UVLPlayground/src/config.ts
@@ -1,4 +1,4 @@
 export default {
-    port: 8010,
+    port: 30000,
     languageServerHostName: "localhost",
 };