Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
mergify: merge, but rebase PR onto master instead of merging
Rebasing the PR will remove the pull request number from history, so we merge. But we can remove the second merge, where mergify merges the (conflict-free) master into the PR before doing CI. Instead, mergify should rebase (`strict_method = rebase`). The [mergify documentation](https://doc.mergify.io/actions.html#merge) has two warnings about strict_method rebase: * GitHub branch protection of your repository may dismiss approved reviews. * GitHub branch protection of the contributor repository may refuse Mergify to force push the rebased pull request. As clarified in Mergifyio/mergify#115 (comment) this only applies to contributors who manually untick the “allow maintainers to modify my branch” (or similar) option. Since that is not the default, we can require PR authors to either have it ticked or rebase their PR manually when mergify requests it.
- Loading branch information