Re: insteadOf and git-request-pull output

Konstantin Ryabitsev [off-list ref] writes:

On Thu, Nov 15, 2018 at 07:54:32PM +0100, Ævar Arnfjörð Bjarmason wrote:

quoted

quoted

I think that if we use the "principle of least surprise," insteadOf
rules shouldn't be applied for git-request-pull URLs.

I haven't used request-pull so I don't have much of an opinion on this,
but do you think the same applies to 'git remote get-url <remote>'?

I.e. should it also show the original unmunged URL, or the munged one as
it does now?

I don't know, maybe both? As opposed to git-request-pull, this is not
exposing the insteadOf URL to someone other than the person who set it
up, so even if it does return the munged URL, it wouldn't be unexpected.

Yeah, I think the local "git remote" should show the rewritten URL
(because that information is not available otherwise) and it is OK
to optionally show the original.  Also, I think it would be nice if
request-pull gave external-facing names.  After all, insteadOf
address is for your own use (e.g. maybe pointing at corporate
mirror), and not for the intended recipient of request-pull.

In short, I think I agree with things you are saying in this
exchange.