How to get your PR merged

1. Create you PR (ideally ask in an issue if that is a good idea what you want to do)
2. Wait for a maintainer review
3. Do the requested changes, and answer any questions raised by the reviewer(s)
4. Rebase on dev if necessary:

$ git checkout dev
$ git pull
$ git checkout <the_branch_im_working_in>
$ git rebase dev
$ # The rebase might consist of several commits, so you might have to do this several times after resolving a collision:
$ git rebase --continue
$ # Check if everything works, and no tests fail.
$ git push --force
$ # WARNING: it will push your local changes and erase the difference. It is needed after a rebase.