Closed Rida-Hamadani closed 1 month ago
As scripts/mk_all.sh is deprecated, and might even get removed with mathlib4#14540.
scripts/mk_all.sh
As
scripts/mk_all.sh
is deprecated, and might even get removed with mathlib4#14540.