Re: [PATCH] push: Alias pushurl from push rewrites

[Junio C Hamano <gitster@pobox.com>]

Jonathan Nieder <jrnieder@gmail.com> writes:

> Sorry, typo.  The configuration in the example above should have been
>
> 	[url "git://anongit.myserver.example.com/"]
> 		insteadOf = myserver.example.com:
> 	[url "myserver.example.com:"]
> 		pushInsteadOf = myserver.example.com:
>
> In other words, suppose I set url.*.insteadof to point to a faster
> address for fetching alongside url.*.pushinsteadof requesting that the
> original address should still be used for pushing.

I didn't know we were even shooting for supporting the identity
mapping:

	url.X.pushinsteadof=X

but that would certainly be nice.

By the way, it seems that the original commit 1c2eafb89bca (Add
url.<base>.pushInsteadOf: URL rewriting for push only, 2009-09-07)
wanted to explicitly avoid use of pushInsteadOf aliasing for a
pushURL and it is also documented in config.txt from day one.

I think the intent is "You have a normal URL, and a way to override
it explicitly with pushURL, or a way to rewrite it via the aliasing
the normal URL with pushInsteadOf. Either one or the other, but not
both, as having many levels of indirection would be confusing."

Which I can understand and sympathise.

In anay case, the change proposed in this thread seems to change
that, so the documentation would need to be updated.  Also the tests
the original commit adds explicitly checks that pushInsteadOf is
ignored, which may have to be updated (unless that test is already
broken).