Yishuai Li (Jan 19 2021 at 17:17): Yishuai Li (Jan 19 2021 at 17:17):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)
Gaëtan Gilbert (Jan 19 2021 at 17:20):that's not the bot, it's a github action thing https://github.com/coq/coq/pull/12832
Yishuai Li (Jan 19 2021 at 17:23):That's what I'm looking for. Thanks!
Théo Zimmermann (Jan 19 2021 at 17:38):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.
Théo Zimmermann (Jan 19 2021 at 17:39):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