--- a/src/Tools/VSCode/src/vscode_setup.scala Sat Feb 26 21:59:12 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala Sat Feb 26 22:00:22 2022 +0100
@@ -48,7 +48,7 @@
"editor.renderIndentGuides": false,
"editor.rulers": [80, 100]
}
-""".stripMargin)
+""")
}
}