Github build failed with no diagnostics

Stream: general

[Eric Wieser]

Any idea what happened here?

https://github.com/leanprover-community/mathlib/runs/2350890535?check_suite_focus=true

[Kevin Buzzard]

This happened to me too, and then a few hours later I got a diagnosis. @Gabriel Ebner do you think this is something to do with the recent "build twice" idea?

[Gabriel Ebner]

I think this is a github issue. If it was on our end, there would be a build log.

[Kevin Buzzard]

Here's my version: https://github.com/leanprover-community/mathlib/runs/2346014022 . I take back my assertion that it started working later -- this must have been another commit.