Commit 2024-10-25 00:50 a1578ecc
View on Github →chore: use Batteries
test driver directly in the lake file (#15897)
With leanprover/lean4#4261, we can specify a test driver from a dependency. We do this with Batteries
test driver. Previously, the test driver from Batteries
was called via scripts/test.lean
which is now removed.