max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lean.code-workspace: fix terminal cwd (#10802)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-10-16 22:19:12 +02:00 • committed by GitHub
parent 8a1b6e0f71
commit 5c7b003191
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
lean.code-workspace
View file

@ -15,7 +15,8 @@
],
"settings": {
// Open terminal at root, not current workspace folder
"terminal.integrated.cwd": "${workspaceFolder:.}",
// (there is not way to directly refer to the root folder included as `.` above)
"terminal.integrated.cwd": "${workspaceFolder:src}/..",
"files.insertFinalNewline": true,
"files.trimTrailingWhitespace": true,
"cmake.buildDirectory": "${workspaceFolder}/build/release",