Skip to content

Commit f650072

Browse files
committed
fix: download oleans from main cache before fork cache (leanprover-community#25682)
1 parent 3b2e97b commit f650072

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Cache/Requests.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -229,9 +229,9 @@ def getFiles
229229
else
230230
let repo ← getRemoteRepo (← read).mathlibDepPath
231231
IO.println s!"Mathlib repository: {repo}"
232-
downloadFiles repo hashMap forceDownload parallel (warnOnMissing := false)
233232
unless repo == MATHLIBREPO do
234-
downloadFiles MATHLIBREPO hashMap forceDownload parallel (warnOnMissing := true)
233+
downloadFiles MATHLIBREPO hashMap forceDownload parallel (warnOnMissing := false)
234+
downloadFiles repo hashMap forceDownload parallel (warnOnMissing := true)
235235
if decompress then
236236
IO.unpackCache hashMap forceUnpack
237237
else

0 commit comments

Comments
 (0)