author | wenzelm |
Mon, 28 Feb 2022 14:29:23 +0100 | |
changeset 75171 | 96b26b0d2cc5 |
parent 75170 | 08b8c0a2d67c |
child 75172 | 26ac98871d42 |
--- a/src/Tools/VSCode/src/vscode_setup.scala Mon Feb 28 14:26:44 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Mon Feb 28 14:29:23 2022 +0100 @@ -81,6 +81,7 @@ "editor.lineNumbers": "off", "editor.renderIndentGuides": false, "editor.rulers": [80, 100], + "editor.unicodeHighlight.ambiguousCharacters": false, "extensions.autoCheckUpdates": false, "extensions.autoUpdate": false, "update.mode": "none"