I like Coqbot's "need: rebase" feature. Is there a smaller bot just to label and unlabel PRs? or should I just install Coqbot in my arbitrary repo? (sounds like killing mosquito with a hammer)
that's not the bot, it's a github action thing https://github.com/coq/coq/pull/12832
That's what I'm looking for. Thanks!
In the Coq repo, the bot does part of it: adds / removes the label when you update a PR and there is a conflict / no more conflicts.
But indeed, you don't need the bot for this feature: the GitHub action is enough.
Last updated: Jun 04 2023 at 22:30 UTC