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.
Sometimes you just don't want coqbot to say anything.
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: Mar 02 2024 at 16:01 UTC