author | wenzelm |
Fri, 18 Feb 2022 12:18:41 +0100 | |
changeset 75090 | 2af8426e1f65 |
parent 75089 | 1e230ff31fb0 |
child 75091 | 445ec26fe47f |
lib/Tools/vscode | file | annotate | diff | comparison | revisions |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/vscode Fri Feb 18 12:18:41 2022 +0100 @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: run Isabelle/VSCode using local VSCodium installation + +DIR="$(isabelle vscode_setup -C)" || exit "$?" +exec "$DIR/bin/codium" \ + --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS")" \ + --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \ + "$@"