Skip to content

Commit 6fdae20

Browse files
bryangingechenReemMelamed
authored andcommitted
chore(Cache): add BatteriesRecycling to isPartOfMathlibCache (leanprover-community#40366)
This is needed for the toolchain bump in leanprover-community#40358. There, the cache verification step was failing because oleans for the new `BatteriesRecycling` module (added in leanprover-community/batteries#1792) were not being uploaded. This needs to be done in a separate PR because the cache verification step uses the toolchain from `master`.
1 parent 58a54ab commit 6fdae20

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Cache/IO.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ TODO: write a better predicate. -/
2929
def isPartOfMathlibCache (mod : Name) : Bool := #[
3030
`Mathlib,
3131
`Batteries,
32+
`BatteriesRecycling,
3233
`Aesop,
3334
`Cli,
3435
`ImportGraph,

0 commit comments

Comments
 (0)