Def getAll

Modification history

2024-06-01 12:47

scripts/mk_all.lean

refactor: tweak and move functionality for getting all modules out of `scripts` (#13339) …

Deleted getAll View on Github →

2024-05-29 17:17

scripts/mk_all.lean

feat: `lake exe mk_all` as a Lean executable (#11853) …

Added getAll View on Github →