From: Junio C Hamano <gitster@pobox.com>
Date: Sun, 07 Jun 2009 04:19:34 GMT
Subject: Re: [WIP/RFC] Allow push and fetch urls to be different
Message-ID: <7vtz2sbrqh.fsf@alter.siamese.dyndns.org>
In-Reply-To: <1244299395-6605-1-git-send-email-git@drmicha.warpmail.net>

Michael J Gruber <git@drmicha.warpmail.net> writes:

> This introduces a config setting remote.$remotename.pushurl which is
> used for pushes only. If absent remote.$remotename.url is used for
> pushes and fetches as before.
> This is useful, for example, in order to to do passwordless fetches
> (remote update) over git: but pushes over ssh.
>
> Signed-off-by: Michael J Gruber <git@drmicha.warpmail.net>
> ---
> This is a working prototype, but I'd like to rfc about the approach before
> coding further.

As I am guilty for suggesting this, obviously I do not have a problem with
what the patch wants to achieve.

And the change looks simple, straightforward and correct.

> Things that would go in a full series:
> * documentation (man pages, maybe manual)
> * tests

Surely.

> * teach builtin-remote about pushurl

Hmm,...  my impression was that "git remote" does not have much support
for the push side.  What kind of things are you going to teach?