author | wenzelm |
Mon, 28 Feb 2022 13:10:22 +0100 | |
changeset 75167 | 0a300751fdf5 |
parent 75166 | 1f6da5d18340 |
child 75168 | ff60b4acd6dd |
child 75169 | b61dc9070344 |
--- a/src/Tools/VSCode/src/vscode_setup.scala Mon Feb 28 13:02:40 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Mon Feb 28 13:10:22 2022 +0100 @@ -81,9 +81,9 @@ "editor.lineNumbers": "off", "editor.renderIndentGuides": false, "editor.rulers": [80, 100], - "update.mode": "none", "extensions.autoCheckUpdates": false, - "extensions.autoUpdate": false + "extensions.autoUpdate": false, + "update.mode": "none" } """