author | Thomas Lindae <thomas.lindae@in.tum.de> |
Thu, 18 Jul 2024 01:18:43 +0200 | |
changeset 81080 | 4aa4bd946f96 |
parent 81079 | ff813e8a3271 |
child 81081 | 6aafcdc0217f |
--- a/src/Tools/VSCode/src/vscode_main.scala Thu Jul 18 22:08:46 2024 +0200 +++ b/src/Tools/VSCode/src/vscode_main.scala Thu Jul 18 01:18:43 2024 +0200 @@ -148,6 +148,7 @@ "editor.renderIndentGuides": false, "editor.renderWhitespace": "none", "editor.rulers": [80, 100], + "editor.quickSuggestions": { "strings": "on" }, "editor.unicodeHighlight.ambiguousCharacters": false, "extensions.autoCheckUpdates": false, "extensions.autoUpdate": false,