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 <gits...@pobox.com> wrote: > Gilberto Stankiewicz <kie...@gmail.com> 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 >
