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
2026-03-02 22:42:13 +00:00
2022-03-18 15:28:20 +01:00
2024-07-26 18:24:06 +02:00
2026-02-11 01:17:40 +00:00
2026-02-11 01:17:40 +00:00
2024-08-23 09:13:27 +00:00
Description
No description provided
Readme 5 GiB
Languages
Lean 94.3%
C++ 4.1%
Python 0.6%
Shell 0.4%
CMake 0.3%