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

[Rob Hoelz <rob@hoelz.ro>]

On Wed, 27 Mar 2013 15:07:18 -0700
Junio C Hamano <gitster@pobox.com> wrote:

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

My use case is that I use Github for my personal development.  I have a
prefix for my personal repos (hoelzro: -> git://github.com/hoelzro for
fetch, git@github.com:hoelzro/ for push) and one for all other Git repos
(github: -> git://github.com/)  I have a few projects where I work in a
fork, but I want to fetch updates from the original project.  So my url
for the origin remote is github:org/project, but my pushurl is
hoelzro:project.  This behavior in Git currently doesn't allow me to
work that way.  I used to work with two remotes; origin for my repo and
base for the official one, but I've found that I prefer this other way.

The test that checked that pushInsteadOf + pushurl shouldn't work as I
expect was actually broken; I have removed it, updated the
documentation, and sent a new patch to the list.

-Rob