# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1721242587 -7200
# Node ID f2e7e240c4249523ad178250288cb2607cbb8d4c
# Parent  f0341e6b1b306bb85e8bf1f07ec8ae652fce2ecc
vscode: disabled whitespace rendering by default because the whitespace symbol is not monospace;

diff -r f0341e6b1b30 -r f2e7e240c424 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Tue Jul 09 16:47:48 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_main.scala	Wed Jul 17 20:56:27 2024 +0200
@@ -146,6 +146,7 @@
     "editor.fontSize": 18,
     "editor.lineNumbers": "off",
     "editor.renderIndentGuides": false,
+    "editor.renderWhitespace": "none",
     "editor.rulers": [80, 100],
     "editor.unicodeHighlight.ambiguousCharacters": false,
     "extensions.autoCheckUpdates": false,