On the question of how to add to a PR locally, have a look at this: https://help.github.com/articles/checking-out-pull-requests-locally/
Github (like the other git hosting services) make PRs available under a well known branch name. So for a given 'ID', you'd do something like: git fetch origin pull/ID/head:BRANCHNAME git checkout BRANCHNAME <hack ... hack; git add ...; git commit; possible git merge> Then either push to your own repo and open a new PR (if one does not have commit access to the central repo), or just push to the central repo if you have commit access to it. DF _______________________________________________ Gnustep-dev mailing list Gnustep-dev@gnu.org https://lists.gnu.org/mailman/listinfo/gnustep-dev
