lib/Tools/vscode
author wenzelm
Fri, 18 Feb 2022 16:56:56 +0100
changeset 75098 9e79c9f55edd
parent 75090 2af8426e1f65
child 75170 08b8c0a2d67c
permissions -rwxr-xr-x
clarified directory;
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" \
75098
9e79c9f55edd clarified directory;
wenzelm
parents: 75090
diff changeset
     9
  --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \
75090
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
  "$@"