Commit 2024-04-02 09:29 23bc40b6
View on Github →feat: add mk_all file (#11781)
Typing ./scripts/mk_all.sh updates the files
Mathlib.lean
MathlibExtras.lean
Mathlib/Tactic.lean
Counterexamples.lean
Archive.lean
so that they import all the available .lean files.
Zulip thread