Weird, it was not working for me earlier today, but now it works.
Thank you,
Gilberto
On Tue, Oct 17, 2017 at 5:57 PM, Junio C Hamano wrote:
> Gilberto Stankiewicz writes:
>
>> I am trying to clone git://repo.or.cz/git-gui.git as described at
>> https://github.com/git/git/blob/master/Documentation/SubmittingPatches
>> but it seems the repo does not exist.
>
> $ git fetch -v git-gui
> Looking up repo.or.cz ... done.
> Connecting to repo.or.cz (port 9418) ... 195.113.20.142 done.
> From git://repo.or.cz/git-gui
> = [up to date]master -> git-gui/master
> = [up to date]pu -> git-gui/pu
> = [up to date]todo -> git-gui/todo
>
> $ git fetch -v git://repo.or.cz/git-gui.git
> Looking up repo.or.cz ... done.
> Connecting to repo.or.cz (port 9418) ... 195.113.20.142 done.
> From git://repo.or.cz/git-gui
> * branch HEAD -> FETCH_HEAD
>