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: Jan 31 2023 at 10:01 UTC