lib/Tools/vscode
author wenzelm
Fri, 18 Feb 2022 12:18:41 +0100
changeset 75090 2af8426e1f65
child 75098 9e79c9f55edd
permissions -rwxr-xr-x
run Isabelle/VSCode using local VSCodium installation;
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" \
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
     9
  --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS")" \
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
    10
  --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \
2af8426e1f65 run Isabelle/VSCode using local VSCodium installation;
wenzelm
parents:
diff changeset
    11
  "$@"