vscode: added default setting to make completions pop up by themselves;
authorThomas Lindae <thomas.lindae@in.tum.de>
Thu, 18 Jul 2024 01:18:43 +0200
changeset 81080 4aa4bd946f96
parent 81079 ff813e8a3271
child 81081 6aafcdc0217f
vscode: added default setting to make completions pop up by themselves;
src/Tools/VSCode/src/vscode_main.scala
--- 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,