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

What's the constructive suggestion for improvement we can draw from this
after all?  Should we deprecate the defaulting of "origin" so that
everybody now should always say "git pull $where"?

branch.*.remote would still provide a default, wouldn't it?  And if 
master is by default set up to track origin/master, the behavior 
wouldn't change.

In other words, make
people more aware that what _they_ do is the special case to have only one
remote to interact with?

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".

Paolo