Commit 2025-04-21 15:04 0c3e3bc3
View on Github →feat(Shake): autodetect the module(s) to shake (#24255) There were still a few references to Mathlib in shake, in particular it had Mathlib hardcoded as the default module to shake. Instead ask Lake what the default targets are. This is a back(?)port of https://github.com/leanprover-community/batteries/pull/1205. These changes themselves should probably be merged anyway, and do not depend on which repository shake ends up in. (Also remove a reference to Mathlib from the help text. We still have Mathlib as an example usage, which I think is innocent enough and can stay.)