You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: vscode-lean4/package.json
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -73,7 +73,7 @@
73
73
"lean4.envPathExtensions": {
74
74
"type": "array",
75
75
"default": [],
76
-
"markdownDescription": "Additional entries to add to the PATH variable of the Lean 4 VS Code extension process and any of its child processes.",
76
+
"markdownDescription": "Additional entries to add to the PATH variable of the Lean 4 VS Code extension process and any of its child processes. Relative paths are resolved against each workspace folder.",
77
77
"items": {
78
78
"type": "string",
79
79
"description": "Entry to add to the PATH variable"
0 commit comments