Proposing new GitHub labels for branches

[Jan Hentschel]

As we’re using GitHub PRs more and more (and not only for getting changes into 
master), I would like to propose the introduction of GitHub labels to mark the 
target branch of a PR, such as “branch-2” for a PR going to branch-2. This 
would make it easier on the PR overview page to see the target branch of a PR 
without opening the PR itself. In a second step we can automate it to let 
GitHub label PRs for us instead of doing it manually. Any objections?