Usage of PRs

[Nyholm]

I believe it is important that everybody, including us maintainers, is using PRs when making changes to a repository. When we use PRs everybody gets notified about the change. Minor changes could of course be merged directly, but we should always use PRs.