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

From: Junio C Hamano <[email-masked]>
Date: Sat, 26 Apr 2008 10:46:16 -0700

"Shawn O. Pearce" <[email-masked]> writes:

> Why not just have a remote named "my-mirror" and do `git push my-mirror`?
> Yes, its on keystroke longer to type.  Call it foo.  `git push foo` would
> be shorter, and not require code changes in Git.

Configuring to push to multiple can already be done as you described, not
having to have a special case code like this patch is certainly very
attractive, and also it is one less "magic" applied to the configuration
(meaning, when you have to figure out what an unadorned "git push" does
for somebody else who is having trouble, you have one less thing to
consider).

I've been torn between

 (1) but then you have to have an extra 'foo' remote and with this patch
     it becomes unnecessary, and

 (2) no, by separating individual remotes (which are not 'foo') and a
     magic "pushing to everywhere" (which is 'foo'), that extra 'foo'
     simplifies things, to explain, understand, and diagnose (when
     something goes south).

I am leaning towards the latter argument now, especially after you
commented on this issue.