GitHub auto-merge is now enabled

[ambv (Łukasz Langa)]

We used to rely on miss-islington’s automatic merging functionality for a long while. We thank her for her service. Today we’re switching to GitHub’s built-in auto-merge functionality. You can expect it to be much more eager to auto-merge PRs. Maybe even a little too eager!

miss-islington will no longer merge any PRs – neither her own backport PRs, nor PRs by other people that have the automerge label. (The automerge label has now been removed.)

To enable auto-merge on a PR

1. Click on the gray “Enable auto-merge” button at the bottom of the PR.

To disable auto-merge on a PR

1. Click on the gray “Disable auto-merge” button at the bottom of the PR.

To pause auto-merge on a PR

Either:

1. Apply a DO-NOT-MERGE label; or,
2. Submit a review requesting changes (red).

Note the difference between disabling automerge entirely, and pausing automerge using the labels. If DO-NOT-MERGE gets removed, auto-merge will resume. If the red review gets addressed, auto-merge will resume.

Documentation

This is all covered in the Dev Guide:

Git Bootcamp and Cheat Sheet

[encukou (Petr Viktorin)]

Fellow users of the mailing list mode, note that the post has been edited.

To enable auto-merge on a PR: Click on the gray “Enable auto-merge” button at the bottom of the PR.
(No need to add a “green” review.)