mathlib3
7dad872f - feat(ci): try fetching olean caches from older commits (#2278)

Commit
5 years ago
feat(ci): try fetching olean caches from older commits (#2278) * feat(ci): try fetching older branch oleans * docstring edits for set_theory.surreal * debug * debug 2 * formatting * try fetching * just increase depth * improve script, improve surreal docstrings * env context * quieter curl * fix overwriting * git clean * ci test: delete surreal.lean * fix env var GIT_HISTORY_DEPTH * add back surreal * reviewer comments Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Parents
Loading