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 :)
