lib/Tools/node
author wenzelm
Sun, 15 Sep 2024 16:45:13 +0200
changeset 80882 2cdb00f797b1
parent 75285 2b64d5657592
permissions -rwxr-xr-x
performance tuning: cache for highly redundant markup (types and sorts);
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