Ali Caglayan (May 09 2022 at 16:29): 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.
Ali Caglayan (May 09 2022 at 16:29):Sometimes you just don't want coqbot to say anything.
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: May 28 2023 at 18:29 UTC