Def Cache.Requests.getRepoFromRemote

Modification history

2026-04-12 01:02
Cache/Requests.lean
feat: cache only emits a warning when Git is not found (#37847) …
Modified Cache.Requests.getRepoFromRemoteView on Github →
2025-06-24 04:54
Cache/Requests.lean
feat: cache uses the nightly-testing cache when relevant (#26334) …
Added Cache.Requests.getRepoFromRemoteView on Github →