mk_all failure aborting the build

Stream: mathlib4

[Ruben Van de Velde]

We used to have a really nice setup where forgetting to add a new file to Mathlib.lean would give you a CI failure, but would also fix it for you and give you results from the actual build. It seems we lost that at some point. Was that intentional?

[Damiano Testa]

I don't think that this is intentional, but I remember someone commenting on the reason this happened (although I forget what it was) very recently, I think within the last week or so...

[Damiano Testa]

Actually, I probably read about it in #13617 -- even though this is not exactly the automation that you are asking for, it might be useful.

[Damiano Testa]

In any case, in general, I am trying to get more tools to help "self-correct" code.