Question About the Merging Process

[Maria Sable]

Hi all,

Sorry if this is a dumb question. I looked at the Contributing page on the
Servo wiki and was not able to find an answer for it.

Once I have a pull request with an approving review, do I need to take any
additional steps to get it merged into master? Or will the person who
reviewed it merge it?

Kind regards,
Maria Sable

[Manish Goregaokar]

The reviewer has to leave a comment saying `@bors-servo r+` to inform our
bot that the pull request needs merging. Once that happens, you can wait.

If you have an approving Github review but no r+, make sure you've
addressed any straggling issues and ping the reviewer.

-Manish Goregaokar

> _______________________________________________
> dev-servo mailing list
> dev-...@lists.mozilla.org
> https://lists.mozilla.org/listinfo/dev-servo
>

[Maria Sable]

Hi Manish,

Thank you! By ping, do you mean @them in the pull request conversation?

Kind regards,
Maria Sable

On Mon, Apr 29, 2019 at 7:26 PM Manish Goregaokar <manis...@gmail.com>
wrote:

[Manish Goregaokar]

Yep!