Stream: Coq devs & plugin devs

Topic: Why github actions and coqbot?

view this post on Zulip Ali Caglayan (Jul 23 2021 at 17:12):

I noticed in https://github.com/coq/coq/pull/14654#issuecomment-885772271 that both coqbot and github actions are putting a needs: rebase label. Should we disable github actions doing this?

view this post on Zulip Gaëtan Gilbert (Jul 23 2021 at 17:14):

coqbot is in charge of removal, github in charge of adding iirc

view this post on Zulip Théo Zimmermann (Jul 23 2021 at 17:35):

coqbot adds the needs: rebase label when a PR is updated but conflicts with the base and removes it when a PR is updated and doesn't conflict anymore.

view this post on Zulip Théo Zimmermann (Jul 23 2021 at 17:36):

The GitHub Action adds the needs: rebase label when the base is updated and introduces conflicts with an existing PR.

Last updated: Dec 07 2023 at 09:01 UTC