# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1721258323 -7200
# Node ID 4aa4bd946f96b65c8e35ce9c2d91ba2171130897
# Parent  ff813e8a32715d78c03d426e911f4b475cdb9dd5
vscode: added default setting to make completions pop up by themselves;

diff -r ff813e8a3271 -r 4aa4bd946f96 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,