chore: make version that setting is used in explicit

leanprover · Oct 13, 2023 · 180730f · 180730f
1 parent 5f678ea
commit 180730f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -67,7 +67,7 @@
 				"lean4.automaticallyBuildDependencies": {
 					"type": "boolean",
 					"default": false,
-					"markdownDescription": "Enable automatically building dependencies when opening a file."
+					"markdownDescription": "Enable automatically building dependencies when opening a file. This is the default for Lean 4 versions before 4.2.0."
 				},
 				"lean4.serverEnv": {
 					"type": "object",