Thanks for both answers. I will do this. It's just weird that it only happened with the one Savannah repo.
Thanks, Arnold Bruno Haible <[email protected]> wrote: > > The workaround is to append the following lines to your $HOME/.gitconfig: > > > > # See > > # > > https://git-scm.com/docs/git-config#Documentation/git-config.txt-urlltbasegtinsteadOf > > # https://git-scm.com/docs/git-clone#_git_urls > > [url "git://git.git.savannah.gnu.org/"] > > insteadOf = git://git.savannah.gnu.org/ > > [url "https://https.git.savannah.gnu.org/git/";] > > insteadOf = https://git.savannah.gnu.org/git/ > > [url "https://github.com/coreutils/gnulib.git";] > > insteadOf = git://git.savannah.gnu.org/gnulib.git > > insteadOf = https://git.savannah.gnu.org/git/gnulib.git > > Alternatively, issue the following commands: > > git config set --global --append > url.git://git.git.savannah.gnu.org/.insteadOf git://git.savannah.gnu.org/ > git config set --global --append > url.https://https.git.savannah.gnu.org/git/.insteadOf > https://git.savannah.gnu.org/git/ > git config set --global --append > url.https://github.com/coreutils/gnulib.git.insteadOf > git://git.savannah.gnu.org/gnulib.git > git config set --global --append > url.https://github.com/coreutils/gnulib.git.insteadOf > https://git.savannah.gnu.org/git/gnulib.git > > This way, you don't have to edit $HOME/.gitconfig by hand. > > Bruno > >
