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" }