author | wenzelm |
Sat, 12 Mar 2022 23:21:28 +0100 | |
changeset 75273 | f1c6e778e412 |
parent 75257 | d1e5f9dbf885 |
child 75277 | f64725832d63 |
permissions | -rwxr-xr-x |
#!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: run Isabelle/VSCode (requires "vscodium-X.YY.Z" component) isabelle vscode_setup || exit "$?" exec "$ISABELLE_VSCODIUM_HOME/vscodium" \ --locale en-US \ --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \ "$@"