# HG changeset patch # User wenzelm # Date 1646054963 -3600 # Node ID 96b26b0d2cc5fb8b1dd300462929887aaa5ef054 # Parent 08b8c0a2d67cc9c5f718254daf92bf81354772c4 clarified rendering; diff -r 08b8c0a2d67c -r 96b26b0d2cc5 src/Tools/VSCode/src/vscode_setup.scala --- 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"