On Thu, Mar 9, 2023 at 8:49 AM Paul Smith <psm...@gnu.org> wrote: > > On Thu, 2023-03-09 at 15:54 +0100, Bruno Haible wrote: > > If you have a checkout of GNU gnulib, in order to successfully do a > > "git pull" again, you will have to change the .git/config file, > > Is it better to suggest Git's CLI interface for this, than edit the > file? > > For example > > git remote set-url $(git remote) https://git.savannah.gnu.org/git/gnulib.git > > ? > > I personally prefer git.sv.gnu.org but I don't like to type :)
I've preferred the .sv.-abbreviated names for a long time, but recently they've caused trouble with mismatched certificates, so I've been switching to the fully-spelled-out host names.
