[phobos] amending a push request

[Jonathan M Davis]

On Sunday 06 March 2011 18:12:38 Andrei Alexandrescu wrote:
> So I have this push request with comments from Jonathan. How do I
> proceed about changing it?

You mean pull request? Just update the code on your local box and commit it on 
your box like you would normally (on the same branch that you've been doing the 
other work on). Then you simply push it to the branch on github like you did 
before. It will update the current pull request.

A pull request is a request to pull from a particular branch from a particular 
repository, not to pull a specific set of commits. It just pulls in whatever 
commits are unique to that branch. So, if you update that branch, it updates the 
pull request.

- Jonathan M Davis