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.

Estimated changes