Def moreLeanArgs

Modification history

2023-12-02 07:05
lakefile.lean
chore: bump Mathlib to Lean v4.4.0-rc1 (#8781) …
Deleted moreLeanArgsView on Github →
2023-07-17 23:40
lakefile.lean
fix: make `warningAsError` a weak arg (#5970)
Modified moreLeanArgsView on Github →
2023-04-24 23:44
lakefile.lean
fix: enable ↦ in server mode (#3556) …
Added moreLeanArgsView on Github →