Andreas Schwab <schwab@xxxxxxxxxxxxxx> writes:
> Junio C Hamano <gitster@xxxxxxxxx> 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.
--
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html