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

From: Junio C Hamano <gitster@pobox.com>
Date: Jan 16, 2013, 20:01 UTC
Message-ID: <7vr4lkx5gq.fsf@alter.siamese.dyndns.org>
In-Reply-To: <m2ip6x0vtk.fsf@igel.home>

Andreas Schwab <schwab@linux-m68k.org> writes:

Show 13 quoted lines

> Junio C Hamano <gitster@pobox.com> writes:
>
>> I actually think my earlier "it shouldn't be the same (push)" is not
>> needed and probably is actively wrong.  Just like you can tell
>> between
>>
>>     (only one .url)                     (both .url and .pushurl)
>>
>>     origin there (fetch/push)           origin there (fetch)
>>                                         origin there (push)
>
> What should happen when you have a .pushinsteadof configured that
> modifies .url for pushing?

I think push should work like this:

 * the user gives us a nickname;

 * we look at remote.$nickname.pushurl (and if there isn't,
   remote.$nickname.url) to decide the logical URLs to push to;

 * for each logical URL we decided to push, we look at
   url.*.pushInsteadOf to see if there is one that match the $URL
   (and if there isn't url.*.insteadOf), and map the logical URL to
   the final destination.

So that we can instruct "push" to push, when pushing into a repository that logically resides at git://git.k.org/pub/, to instead push into the repository via git-over-ssh, e.g.

    [remote "korg"]
	url = git://git.k.org/pub/scm/git/git.git/

    [url "git.k.org:/pub/"]
        pushInsteadOf = git://git.k.org/pub/

without affecting the fetching side.

As I said in a separate message, the above "fetch/push" vs "fetch" and "push" distinction is not descriptive enough to express the post rewriting that is done with insteadOf; it only helps debugging misconfiguration between .url vs .pushurl, which may be better than the status quo but is not ideal.