lib/Tools/node
author wenzelm
Tue, 07 Mar 2023 11:13:36 +0100
changeset 77555 d45a01c41fe2
parent 75285 2b64d5657592
permissions -rwxr-xr-x
tuned structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75283
574fb6486c57 support Node.js as well, reusing the engine from Electron/VSCodium;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
574fb6486c57 support Node.js as well, reusing the engine from Electron/VSCodium;
wenzelm
parents:
diff changeset
     2
#
574fb6486c57 support Node.js as well, reusing the engine from Electron/VSCodium;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
574fb6486c57 support Node.js as well, reusing the engine from Electron/VSCodium;
wenzelm
parents:
diff changeset
     4
#
75284
5417613efd74 tuned messages;
wenzelm
parents: 75283
diff changeset
     5
# DESCRIPTION: run the Node.js framework within the Isabelle environment
75283
574fb6486c57 support Node.js as well, reusing the engine from Electron/VSCodium;
wenzelm
parents:
diff changeset
     6
75285
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
     7
if [ -z "$ISABELLE_VSCODIUM_ELECTRON" ]; then
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
     8
  echo '*** Undefined $ISABELLE_VSCODIUM_ELECTRON: missing "vscodium" component'
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
     9
  exit 2
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
    10
else
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
    11
  export ELECTRON_RUN_AS_NODE=1
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
    12
  exec "$ISABELLE_VSCODIUM_ELECTRON" "$@"
2b64d5657592 clarified errors;
wenzelm
parents: 75284
diff changeset
    13
fi