author | wenzelm |
Mon, 28 Feb 2022 12:41:48 +0100 | |
changeset 75162 | 4fc51c9cf8fd |
parent 75161 | 95612f330c93 |
child 75163 | c440b77c79c0 |
--- a/src/Tools/VSCode/src/vscode_setup.scala Sun Feb 27 20:00:23 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_setup.scala Mon Feb 28 12:41:48 2022 +0100 @@ -46,7 +46,8 @@ "editor.fontSize": 18, "editor.lineNumbers": "off", "editor.renderIndentGuides": false, - "editor.rulers": [80, 100] + "editor.rulers": [80, 100], + "update.mode": "none" } """) }