prefer hardwired locale;
authorwenzelm
Mon, 28 Feb 2022 14:26:44 +0100
changeset 75170 08b8c0a2d67c
parent 75169 b61dc9070344
child 75171 96b26b0d2cc5
prefer hardwired locale;
lib/Tools/vscode
--- 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)" \
   "$@"