equal
deleted
inserted
replaced
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: run the Node.js framework within the Isabelle environment |
5 # DESCRIPTION: run the Node.js framework within the Isabelle environment |
6 |
6 |
7 export ELECTRON_RUN_AS_NODE=1 |
7 if [ -z "$ISABELLE_VSCODIUM_ELECTRON" ]; then |
8 exec "$ISABELLE_VSCODIUM_ELECTRON" "$@" |
8 echo '*** Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component' |
|
9 exit 2 |
|
10 else |
|
11 export ELECTRON_RUN_AS_NODE=1 |
|
12 exec "$ISABELLE_VSCODIUM_ELECTRON" "$@" |
|
13 fi |