diff -r ea4fa50dbb74 -r 35a5c4b16024 src/Tools/VSCode/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/etc/settings	Thu Feb 17 19:00:14 2022 +0100
@@ -0,0 +1,5 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_VSCODE_VERSION="1.64.2"
+ISABELLE_VSCODE_HOME="$ISABELLE_HOME/src/Tools/VSCode"
+ISABELLE_VSCODE_SETTINGS="$ISABELLE_HOME_USER/vscode"