src/Tools/VSCode/etc/settings
author wenzelm
Mon, 07 Mar 2022 17:18:19 +0100
changeset 75239 ef9f9d43b867
parent 75209 4187f6f18232
child 75252 41dfe941c3da
permissions -rw-r--r--
updated to VSCode 1.65.0;

# -*- shell-script -*- :mode=shellscript:

ISABELLE_VSCODE_VERSION="1.65.0"
ISABELLE_VSCODE_HOME="$ISABELLE_HOME/src/Tools/VSCode"
ISABELLE_VSCODE_SETTINGS="$ISABELLE_HOME_USER/vscode"
ISABELLE_VSCODE_WORKSPACE="$ISABELLE_VSCODE_SETTINGS/workspace"