Re: So git pull is shorthand for what exactly?

  On 10/01/2010 01:08 PM, I wrote:
>
>
> "git push origin HEAD" pushes the current branch, whatever it might 
> be. That might be a useful alias for you to set up.
>
>

Oh, and you can change the default by setting push.default to 'current' 
instead of 'matching', which is the default default ;-) "man git-config" 
for details.

cheers

andrew