New script to identify merged branches to delete

Once a PR has been merged, its reference branch is in most cases no
longer needed. GitHub offers a button to delete it, but this is a manual
task and if not done right away developers forget to do it and these
branches tends to pile up.

This script checks all branches in the specified developer's repository
against successfully merged PRs that were submitted by that developer in
the reference repository. If one or more matching references are found,
it prints a command that can be used to delete the no-longer needed
branches.