Kevin Buzzard (Apr 30 2020 at 12:45):
The mathlib github page is currently proudly displaying this:
Is that supposed to happen?
Gabriel Ebner (Apr 30 2020 at 12:50):
We know about it. It is not serious. It will be fixed.
Kevin Buzzard (Aug 02 2020 at 10:41):
CI is failing on master:
Rob Lewis (Aug 02 2020 at 10:44):
I think this must be a glitch.
Kenny Lau (Aug 02 2020 at 11:05):
I clicked the re-run button (wait, I can do that??)
Kenny Lau (Aug 02 2020 at 11:06):
it builds now
Rob Lewis (Aug 02 2020 at 11:09):
Note that CI on master is almost completely unnecessary. It only matters if someone pushes directly to master. There are no CI steps anymore that are master-specific and the same commit has to build in bors' staging branch in order to be merged.
Last updated: May 17 2021 at 22:15 UTC