coq/bot

"needs" and "request full CI" should be removed only after the pipeline is successfully started

Opened this issue · 0 comments

If gitlab is having issues we can end up with no label and no pipeline.