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

From: Junio C Hamano <gitster@pobox.com>
Date: Mar 27, 2013, 22:07 UTC
Message-ID: <7vsj3gjy3t.fsf@alter.siamese.dyndns.org>
In-Reply-To: <20130327211554.GH28148@google.com>

Jonathan Nieder <jrnieder@gmail.com> writes:

Show 10 quoted lines

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