Def Cache.IO.packCache

Modification history

2025-02-11 14:10
Cache/IO.lean
chore(Cache): rename HashMap to ModuleHashMap (#21704) …
Modified Cache.IO.packCacheView on Github →
2024-02-09 21:00
Cache/IO.lean
chore: cache: do not try to upload files just downloaded (#9687) …
Modified Cache.IO.packCacheView on Github →
2024-01-04 04:39
Cache/IO.lean
fix: partial revert of #9409 (re-enable Azure cache) (#9419) …
Modified Cache.IO.packCacheView on Github →
2023-09-15 00:38
Cache/IO.lean
feat: add git origin info to cache .ltar files (#7143) …
Modified Cache.IO.packCacheView on Github →
2023-01-30 23:47
Cache/IO.lean
fix: curl is not needed for all commands (#1956) …
Added Cache.IO.packCacheView on Github →