We will need the GitHub usernames of anyone who wants to contribute.
Please add your GitHub username in a comment below if you want/need write
access to the repository.
This should be completed BEFORE the move (as this might give us a chance to
also fix ownerships in the issue tracker).
See MoveToGitHub.