Does anybody know what these failures mean? https://gitlab.com/coq/coq/-/pipelines/183273775
pipeline wasn't run for https://github.com/coq/coq/pull/11742 (no clue why)
so the need to set the docker image to build was not noticed
build with docker started https://gitlab.com/coq/coq/-/pipelines/183286962
We should have been triggered by the fact that it is
github-action and not
coqbot who removed the
needs: rebase label!
Anyway, I'll see if I can identify the source of the failure to run this pipeline.
OK it turns out that this was again an occurrence of https://github.com/coq/bot/issues/98. Until we fix this, I wonder if we shouldn't revert https://github.com/coq/bot/pull/89.
Last updated: Oct 16 2021 at 03:02 UTC