changeset 75171 | 96b26b0d2cc5 |
parent 75167 | 0a300751fdf5 |
child 75178 | 01017b938135 |
--- 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"