author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
parent 76020 | 04ce6cf2bd3b |
permissions | -rw-r--r-- |
75083 | 1 |
# -*- shell-script -*- :mode=shellscript: |
2 |
||
76020
04ce6cf2bd3b
update VSCodium 1.65.2 ~> 1.70.1, Electron 13.5.2 ~> 18.3.5, Node.js v14.16.0 ~> v16.13.2;
wenzelm
parents:
75282
diff
changeset
|
3 |
ISABELLE_VSCODE_VERSION="1.70.1" |
75083 | 4 |
ISABELLE_VSCODE_HOME="$ISABELLE_HOME/src/Tools/VSCode" |
5 |
ISABELLE_VSCODE_SETTINGS="$ISABELLE_HOME_USER/vscode" |