mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
d03499322d
This PR replaces `lean.code-workspace` with standard `.vscode/` configuration files (`settings.json`, `tasks.json`, `extensions.json`). The workspace file required users to explicitly "Open Workspace from File" (and moreover gives a noisy prompt whether or not they want to open it), while `.vscode/` settings are picked up automatically when opening the folder. This became possible after #12652 reduced the workspace to a single folder. Also drops the `rewrap.wrappingColumn` markdown setting, as the Rewrap extension is no longer signed on the VS Code marketplace. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
37 lines
448 B
Plaintext
37 lines
448 B
Plaintext
*~
|
|
\#*
|
|
.#*
|
|
.lake
|
|
lake-manifest.json
|
|
/build
|
|
/src/lakefile.toml
|
|
/lakefile.toml
|
|
GPATH
|
|
GRTAGS
|
|
GSYMS
|
|
GTAGS
|
|
.projectile
|
|
.lean_options
|
|
.vs
|
|
compile_commands.json
|
|
*.idea
|
|
tasks.json
|
|
settings.json
|
|
!.claude/settings.json
|
|
.gdb_history
|
|
.vscode/*
|
|
!.vscode/settings.json
|
|
!.vscode/tasks.json
|
|
!.vscode/extensions.json
|
|
script/__pycache__
|
|
*.produced.out
|
|
CMakeSettings.json
|
|
CppProperties.json
|
|
result
|
|
fwIn.txt
|
|
fwOut.txt
|
|
wdErr.txt
|
|
wdIn.txt
|
|
wdOut.txt
|
|
downstream_releases/
|