elan breaks every now and then

Stream: lean4

[Henrik Böving]

Every now and then Github notifies me about the periodically running doc-gen pipelines failing as can be seen here: https://github.com/leanprover/doc-gen4/actions?query=is%3Afailure+event%3Aschedule++ this appears to be because elan is receiving random 404s. Is this a known thing? It doesn't appear to happen too often, we're at 1.9k ish scheduled runs and only a few have failed so far but I thought I'd bring it up just in case.

[Mac]

I imagine if the doc-gen4 build runs at the same time the lean4 nightly is being released that could lead to errors fetching the latest release (which does appear to be the step hitting the 502/404 errors).