author | wenzelm |
Mon, 28 Feb 2022 14:26:44 +0100 | |
changeset 75170 | 08b8c0a2d67c |
parent 75169 | b61dc9070344 |
child 75171 | 96b26b0d2cc5 |
lib/Tools/vscode | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/vscode Mon Feb 28 14:24:39 2022 +0100 +++ b/lib/Tools/vscode Mon Feb 28 14:26:44 2022 +0100 @@ -6,6 +6,7 @@ DIR="$(isabelle vscode_setup -C)" || exit "$?" exec "$DIR/bin/codium" \ + --locale en-US \ --user-data-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/user-data)" \ --extensions-dir "$(platform_path "$ISABELLE_VSCODE_SETTINGS"/extensions)" \ "$@"