On this PR the bench was completed without coqbot sending a message in the PR. Is it a known issue?
This topic was moved here from #Coq devs & plugin devs > Bench not reported by coqbot by Karl Palmskog.
Sometimes the GitHub web hooks have issues so coqbot is not aware that the bench has finished.
Sorry that would be Gitlab.
I'm not sure how to fire the webhook in Gitlab.
Last updated: May 28 2023 at 18:29 UTC