-
Notifications
You must be signed in to change notification settings - Fork 14
Description
GitHub has a button allowing PR authors and maintainers to rebase the PR branch on develop, or to merge develop into the PR branch. However, there is often a long delay between the tip of develop and the most recent commit for which Gitlab CI has passed. PRs cannot start their own CI until their base commit has finished.
Many core maintainers have their own tricks for rebasing their PR branches on the latest commit for which CI has completed (please share these here!). It would be great if spackbot could do this for me. I don't care too much about naming, but for now I'll propose two new commands:
@spackbot rebase pipeline
@spackbot merge pipeline
to rebase or merge the PR branch to the latest commit for which Gitlab CI has completed. Another question is whether it should be the latest finished commit or the latest passing commit.