Stream: coqbot devs & users

Topic: "Need rebase" bot?


view this post on Zulip 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)

view this post on Zulip 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

Kind: infrastructure. This is an alternative to adding this feature to @coqbot (coq/bot#14).

view this post on Zulip Yishuai Li (Jan 19 2021 at 17:23):

That's what I'm looking for. Thanks!

view this post on Zulip 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.

view this post on Zulip 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: Jan 31 2023 at 11:01 UTC