# HG changeset patch
# User wenzelm
# Date 1646049197 -3600
# Node ID 837bcbe6083706aea599353db1621ae24a28c01a
# Parent  c440b77c79c0d2524b73193d8f1bb5cf866a8b3a
disable extension updates;

diff -r c440b77c79c0 -r 837bcbe60837 src/Tools/VSCode/src/vscode_setup.scala
--- a/src/Tools/VSCode/src/vscode_setup.scala	Mon Feb 28 12:51:27 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_setup.scala	Mon Feb 28 12:53:17 2022 +0100
@@ -42,7 +42,9 @@
   "editor.lineNumbers": "off",
   "editor.renderIndentGuides": false,
   "editor.rulers": [80, 100],
-  "update.mode": "none"
+  "update.mode": "none",
+  "extensions.autoCheckUpdates": false,
+  "extensions.autoUpdate": false
 }
 """