diff --git a/web-ide/ide-server/settings.json b/web-ide/ide-server/settings.json index 1a005dae3b..be7c72b303 100644 --- a/web-ide/ide-server/settings.json +++ b/web-ide/ide-server/settings.json @@ -1,3 +1,4 @@ { - "daml.telemetry": "Enable" + "daml.telemetry": "Enable", + "terminal.integrated.shell.linux": "echo \"No terminal available\"" } diff --git a/web-ide/proxy/static/css/webide.main.css b/web-ide/proxy/static/css/webide.main.css index f22a822e2e..02e1597d1c 100644 --- a/web-ide/proxy/static/css/webide.main.css +++ b/web-ide/proxy/static/css/webide.main.css @@ -59,10 +59,10 @@ div.window-appicon { }*/ /*hide the actual terminal and debug console*/ -.part.panel.bottom ul.actions-container li.action-item[title*="Debug Console"], -.part.panel.bottom ul.actions-container li.action-item[title*="Terminal"], -.part.panel.bottom div.integrated-terminal, -.part.panel.bottom div.repl { +.part.panel ul.actions-container li.action-item[title*="Debug Console"], +.part.panel ul.actions-container li.action-item[title*="Terminal"], +.part.panel div.integrated-terminal, +.part.panel div.repl { display:none !important; }