# HG changeset patch
# User wenzelm
# Date 1646050222 -3600
# Node ID 0a300751fdf564ef0a2ac9153127ad0253d2f048
# Parent  1f6da5d18340b3bb12352ba53c2642e7ff72c37e
tuned;

diff -r 1f6da5d18340 -r 0a300751fdf5 src/Tools/VSCode/src/vscode_setup.scala
--- 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"
   }
 """