Re: [BUG] Possible bug in `remote set-url --add --push`

[Michael J Gruber <git@drmicha.warpmail.net>]

Phil Hord venit, vidit, dixit 16.01.2013 17:15:
> On Tue, Jan 15, 2013 at 10:53 AM, Junio C Hamano <gitster@pobox.com> wrote:
>> Michael J Gruber <git@drmicha.warpmail.net> writes:
>>
>>> That being said, I don't mind changing the behaviour of set-url.
>>
>> I do not think we want to change the behaviour of set-url.
> 
> I agree with Michael that changing the set-url behavior would be
> appropriate here.  If I say "--add" this pushUrl, don't I mean to
> create an additional url which is pushed to?

I said I wouldn't mind, I didn't vote for it.

> I agree that it makes the config situation messy; this is currently a
> "clean" sequence, in that it leaves the config unchanged after both
> steps are completed:
> 
>   git remote set-url --add --push origin /tmp/foo
>   git remote set-url --delete --push origin /tmp/foo
> 
> If the behavior is changed like Michael suggested, it would not leave
> the config clean (unless heroic steps were taken to keep track).  But
> I'm not sure that's such a bad thing.  In simple command sequences,
> the results would be clean and the only behavior change is that the
> initial "--add" really acts like "add" and not "replace".  But more
> complex sequences could be devised which were affected by this change.
> 
> I'm curious, Junio.  Do you think the set-url behavior is correct
> as-is, or that changing it will cause breakage for some workflows, or
> that it complicates the operation too much for people who are already
> used to the config layout?

For "set url --add --push" on top of a push url only being defaulted
from a fetch url, both behaviours (replace or add, i.e. current or new)
make sense to me. So the questions are:

- Is it worth and possible changing?
- How to best describe it in "remote -v" and "remote show" output?

My patch answered to "no" to the first question and answers the second
one in cases where (push)insteadof is not used to transform one fetch
config into two different urls for fetch and push. I think :)

Michael