Skip to content

Commit 5c7b003

Browse files
authored
chore: lean.code-workspace: fix terminal cwd (#10802)
1 parent 8a1b6e0 commit 5c7b003

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

lean.code-workspace

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@
1515
],
1616
"settings": {
1717
// Open terminal at root, not current workspace folder
18-
"terminal.integrated.cwd": "${workspaceFolder:.}",
18+
// (there is not way to directly refer to the root folder included as `.` above)
19+
"terminal.integrated.cwd": "${workspaceFolder:src}/..",
1920
"files.insertFinalNewline": true,
2021
"files.trimTrailingWhitespace": true,
2122
"cmake.buildDirectory": "${workspaceFolder}/build/release",

0 commit comments

Comments
 (0)