As to those who don't have commit access but consider doing pull requests: am I right that they could set up their working copy of the ports tree to use a personal fork on github as the default remote for pushing while still pulling from the official repo? I don't think I've seen that mentioned in the Wiki (but it's quite likely I missed it).
Yes you can. Just fork the repo on GitHub then in your local checkout add this as an additional remote repo. See 'git remote help' for details.
Chris
