How to merge a pull request on GitHub

[Francois-Xavier Bonnet]

Hi all,

How do we merge a pull request on GitHub? What is the process? Is there a
guideline somewhere? Who has the rights?