equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # DESCRIPTION: run Isabelle/VSCode using local VSCodium installation |
5 # DESCRIPTION: run Isabelle/VSCode using local VSCodium installation |
6 |
|
7 export ISABELLE_VSCODE_SYMBOLS="$(platform_path "$ISABELLE_VSCODE_WORKSPACE/symbols.json")" |
|
8 |
6 |
9 DIR="$(isabelle vscode_setup -C)" || exit "$?" |
7 DIR="$(isabelle vscode_setup -C)" || exit "$?" |
10 exec "$DIR/bin/codium" \ |
8 exec "$DIR/bin/codium" \ |
11 --locale en-US \ |
9 --locale en-US \ |
12 --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ |
10 --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ |