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?
coqbot is in charge of removal, github in charge of adding iirc
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.
The GitHub Action adds the
needs: rebase label when the base is updated and introduces conflicts with an existing PR.
Last updated: Oct 16 2021 at 02:03 UTC