Stream: coqbot devs & users

Topic: Bench not reported by coqbot

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 14:56):

On this PR the bench was completed without coqbot sending a message in the PR. Is it a known issue?

view this post on Zulip Notification Bot (Aug 18 2022 at 15:43):

This topic was moved here from #Coq devs & plugin devs > Bench not reported by coqbot by Karl Palmskog.

view this post on Zulip Ali Caglayan (Aug 18 2022 at 17:24):

Sometimes the GitHub web hooks have issues so coqbot is not aware that the bench has finished.

view this post on Zulip Ali Caglayan (Aug 18 2022 at 17:24):

Sorry that would be Gitlab.

view this post on Zulip Ali Caglayan (Aug 18 2022 at 17:24):

I'm not sure how to fire the webhook in Gitlab.

Last updated: May 28 2023 at 18:29 UTC