Commit 2023-11-20 03:02 fd325734

View on Github →

chore: silence tests, and enforce this (#8438)

Estimated changes

Modified GNUmakefile

Modified test/DeriveFintype.lean

Modified test/Expr.lean

Modified test/FBinop.lean

Modified test/Find.lean

Modified test/Imports.lean

Modified test/MaxPowDiv.lean

Modified test/TypeCheck.lean

Modified test/eqns.lean

Modified test/finsupp_notation.lean

Modified test/search/DepthFirst.lean

Modified test/success_if_fail_with_msg.lean

Modified test/symm.lean