src/Tools/VSCode/src/vscode_setup.scala
changeset 75265 481665cc17e6
parent 75257 d1e5f9dbf885
child 75267 6369151119ee
--- a/src/Tools/VSCode/src/vscode_setup.scala	Fri Mar 11 13:17:14 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Fri Mar 11 13:31:46 2022 +0100
@@ -26,6 +26,7 @@
     "editor.unicodeHighlight.ambiguousCharacters": false,
     "extensions.autoCheckUpdates": false,
     "extensions.autoUpdate": false,
+    "files.encoding": "utf8isabelle",
     "terminal.integrated.fontFamily": "monospace",
     "update.mode": "none"
   }