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
4. Rebase with dev if it is 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.