5 Commits

Author	SHA1	Message	Date
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
Sebastian Ullrich	3a0edd05e6	doc: VS Code dev setup (#2961) ... * multi-root workspace * default settings including .lean line length * tasks `build` and `test` --------- Co-authored-by: mhuisi <mhuisi@protonmail.com>	2023-11-30 08:35:03 +00:00
Chris Lovett	2860ba96f5	doc: fix some syntax and link in the docs, and more	2021-10-10 11:36:43 +02:00
Wojciech Nawrocki	43190e0e63	feat: FromToJson for recursive inductives	2021-07-24 10:47:38 +02:00
Wojciech Nawrocki	e89aa5641e	chore: auto-insert newlines	2021-07-05 19:42:01 +02:00