Re: [PATCH resend] make "git push" update origin and mirrors, "git push --mirror" update mirrors

From: Paolo Bonzini <bonzini@gnu.org>
Date: Apr 28, 2008, 05:07 UTC
Message-ID: <48155B7F.8020202@gnu.org>
In-Reply-To: <20080428012613.GB15121@sigill.intra.peff.net>

Show 7 quoted lines

>> I think "git pull" is different, because it is more often fetching from  
>> one defined place (while Shawn said that he has a need for one-to-many  
>> "git push"es and so do I).  For "git pull", the branch config provides a  
>> valuable default more often than for "git push".
> 
> I think it is highly dependent on your workflow. I would have said the
> exact opposite.

Ah, to do so I always do fetch+gitk+merge (or cherry-pick instead of merge). I use "git pull" (without arguments) only when I can blindly not care about what's on the other side, e.g. because it's Junio who assures it is good. :-)

I actually think I never use "git pull" with arguments, but that's evidently me.

Paolo