changeset 75284 | 5417613efd74 |
parent 75283 | 574fb6486c57 |
child 75285 | 2b64d5657592 |
--- a/lib/Tools/node Tue Mar 15 13:16:13 2022 +0100 +++ b/lib/Tools/node Tue Mar 15 13:22:37 2022 +0100 @@ -2,7 +2,7 @@ # # Author: Makarius # -# DESCRIPTION: run the Node.js framework (with its own command-line arguments) +# DESCRIPTION: run the Node.js framework within the Isabelle environment export ELECTRON_RUN_AS_NODE=1 exec "$ISABELLE_VSCODIUM_ELECTRON" "$@"