>> git remote update >> git push --mirror g...@github.com:lilypond/lilypond.git > > Definitely add --prune to "git remote update" to remove branches > that ceased to exist on the remote.
OK, done. > In general, I would not run the mirroring from a real working copy > of the repository because AFAICT git push --mirror will also push > local branches. I don't do that. I have a separate clone for that (created with `git clone --mirror`). > But it doesn't really matter if everybody is ok with me removing > them once I get access. This is fine with me. Werner
