digital-asset/daml
1
1
Fork 0
mirror of https://github.com/digital-asset/daml.git synced 2024-11-04 00:36:58 +03:00
Code Issues Projects Releases Wiki Activity

webide: failing terminal (#1087)

Browse Source 
* fail bash terminal by setting config to run bogus command
* one last fix for hiding terminal

Initially attempted to use external terminal with echo command but this
still opened an integrated terminal. Changing the terminal command from
/bin/bash to echo "No Terminal Available" crashes the integrated
terminal, which of course is better than having a working terminal!
This commit is contained in:
Bolek@DigitalAsset 2019-05-10 15:31:32 -04:00 committed by GitHub
parent fac312dd40
commit 63960bfa85
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
web-ide/ide-server/settings.json
View File

@ -1,3 +1,4 @@
{ {
"daml.telemetry": "Enable" "daml.telemetry": "Enable",
"terminal.integrated.shell.linux": "echo \"No terminal available\""
} }

8
web-ide/proxy/static/css/webide.main.css
View File

@ -59,10 +59,10 @@ div.window-appicon {
}*/ }*/
/*hide the actual terminal and debug console*/ /*hide the actual terminal and debug console*/
.part.panel.bottom ul.actions-container li.action-item[title*="Debug Console"], .part.panel ul.actions-container li.action-item[title*="Debug Console"],
.part.panel.bottom ul.actions-container li.action-item[title*="Terminal"], .part.panel ul.actions-container li.action-item[title*="Terminal"],
.part.panel.bottom div.integrated-terminal, .part.panel div.integrated-terminal,
.part.panel.bottom div.repl { .part.panel div.repl {
display:none !important; display:none !important;
} }