chore: revert accidental change in .vscode/settings.json (leanprover-community#40122)

MichaelStollBayreuth · MichaelStollBayreuth · commit 4d26f56868bc · 2026-06-01T17:20:46.000Z
This reverts an addition to .vscode/settings.json that was inadvertently part of leanprover-community#39127.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -20,7 +20,5 @@
   "files.readonlyInclude": {
     "**/.elan/**": true,
     "**/.lake/**": true
-  },
-  "json.schemaDownload.enable": false,
-  "workbench.experimental.cloudChanges.partialMatches.enabled": true
+  }
 }

Original file line number	Diff line number	Diff line change
`@@ -20,7 +20,5 @@`
`20`	`20`	`"files.readonlyInclude": {`
`21`	`21`	`"/.elan/": true,`
`22`	`22`	`"/.lake/": true`
`23`		`- },`
`24`		`- "json.schemaDownload.enable": false,`
`25`		`- "workbench.experimental.cloudChanges.partialMatches.enabled": true`
	`23`	`+ }`
`26`	`24`	`}`