author | wenzelm |
Fri, 11 Mar 2022 13:31:46 +0100 | |
changeset 75265 | 481665cc17e6 |
parent 75264 | 5cae3e486cec |
child 75266 | 72112cf37bf7 |
--- 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" }