integrate-then-merge by bot

[adriaanm]

add /integrate command, which launches the integration job on the merge commit of PR into target branch, actually merges PR on success

TODO: figure out smoothest way to do this -- ideally, we'd build actual merge comment and then push to repo, but that would mean not using the "merge button", closing the PR instead... maybe that's the way to go

[SethTisue]

fwiw, I would be sorry to lose the purple "merged" indicators on GitHub

[VladUreche]

What @adriaanm is describing is the @bors bot from the Rust team. EDIT: The bot code is open source, available here: https://github.com/buildbot/buildbot

[SethTisue]

GitHub has auto-merge now

it also has a setting to require a branch be up to date before it's merged. we could enable that, but it's not clear it's worth it. 🤷