| author | wenzelm | 
| Fri, 10 Jun 2022 23:53:09 +0200 | |
| changeset 75553 | 4dd0f250ec0d | 
| parent 75285 | 2b64d5657592 | 
| permissions | -rwxr-xr-x | 
#!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: run the Node.js framework within the Isabelle environment if [ -z "$ISABELLE_VSCODIUM_ELECTRON" ]; then echo '*** Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component' exit 2 else export ELECTRON_RUN_AS_NODE=1 exec "$ISABELLE_VSCODIUM_ELECTRON" "$@" fi