equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: run the Electron framework within the Isabelle environment |
5 # DESCRIPTION: run the Electron.js framework within the Isabelle environment |
6 |
6 |
7 if [ -z "$ISABELLE_VSCODIUM_ELECTRON" ]; then |
7 if [ -z "$ISABELLE_VSCODIUM_ELECTRON" ]; then |
8 echo '*** Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component' |
8 echo '*** Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component' |
9 exit 2 |
9 exit 2 |
10 else |
10 else |