Kim Morrison d03499322d chore: replace workspace file with .vscode/ settings (#12770) ...

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>

2026-03-04 01:10:04 +00:00

..

extensions.json

chore: replace workspace file with .vscode/ settings (#12770)

2026-03-04 01:10:04 +00:00

settings.json

chore: replace workspace file with .vscode/ settings (#12770)

2026-03-04 01:10:04 +00:00

tasks.json

chore: replace workspace file with .vscode/ settings (#12770)

2026-03-04 01:10:04 +00:00