Implemented in rust-lang/team#2538. I created this issue to nominate so we can discuss in the next lang team meeting.
We don't use bors, so all three options to merge a pull request appear today. Historically PRs have used merge commits, but this was not enforced.
There's not a need for merge commits in a repo as simple as lang-team, and there's not an option to require them for consistency either. For simplicity, let's disallow future merge commits and keep a linear history.
Implemented in rust-lang/team#2538. I created this issue to nominate so we can discuss in the next lang team meeting.
We don't use bors, so all three options to merge a pull request appear today. Historically PRs have used merge commits, but this was not enforced.
There's not a need for merge commits in a repo as simple as lang-team, and there's not an option to require them for consistency either. For simplicity, let's disallow future merge commits and keep a linear history.