Stream: coqbot devs & users

Topic: "coqbot: mute" label?


view this post on Zulip Ali Caglayan (May 09 2022 at 16:29):

Would it be possible to add a "coqbot: mute" label which stops coqbot from posting when around? Obviously, it should be removed for PRs before merging.

view this post on Zulip Ali Caglayan (May 09 2022 at 16:29):

Sometimes you just don't want coqbot to say anything.

view this post on Zulip Théo Zimmermann (May 10 2022 at 08:09):

So muting all the bot comments at once? Why not indeed? I think it would be even better if coqbot has then another way to express itself, such as through reactions to comments and check runs. Expert users of the bot could still trigger it and have an idea of its state by looking at these other data points, but it would be less noisy.


Last updated: Jan 31 2023 at 10:01 UTC