lib/Tools/vscode
author wenzelm
Wed, 09 Mar 2022 16:21:14 +0100
changeset 75252 41dfe941c3da
parent 75240 83197a0ac6df
child 75257 d1e5f9dbf885
permissions -rwxr-xr-x
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75090
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     2
#
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     4
#
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     6
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     7
DIR="$(isabelle vscode_setup -C)" || exit "$?"
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     8
exec "$DIR/bin/codium" \
75170
08b8c0a2d67c prefer hardwired locale;
wenzelm
parents: 75098
diff changeset
     9
  --locale en-US \
75098
9e79c9f55edd clarified directory;
wenzelm
parents: 75090
diff changeset
    10
  --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \
75090
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
    11
  --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
    12
  "$@"