Re: git push permissions

[Ralf Wildenhues]

Hello,

* Bruno Haible wrote on Sun, Oct 10, 2010 at 05:49:06PM CEST:
>   3. to make a new git checkout of gnulib with the non-anonymous method
>      (see <https://savannah.gnu.org/git/?group=gnulib>).

This is not necessary.  Once Bruce has the required permission, he can

  git remote add write ssh://address@hidden/srv/git/gnulib.git

(with $USER replaced by the appropriate user name)
and then push commits using

  git push --dry-run write master

(remove the --dry-run to actually do the push if the output looks sane).

Use 'git remote update' to fetch from more than one remote.  If more
than one remote are too complex for you, just ignore my message.  ;-)

Cheers,
Ralf