| author | wenzelm |
| Wed, 09 Mar 2022 16:21:14 +0100 | |
| changeset 75252 | 41dfe941c3da |
| parent 75240 | 83197a0ac6df |
| child 75257 | d1e5f9dbf885 |
| permissions | -rwxr-xr-x |
| 75090 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation |
|
6 |
||
7 |
DIR="$(isabelle vscode_setup -C)" || exit "$?" |
|
8 |
exec "$DIR/bin/codium" \ |
|
| 75170 | 9 |
--locale en-US \ |
| 75098 | 10 |
--user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ |
| 75090 | 11 |
--extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \ |
12 |
"$@" |