Werner LEMBERG <[email protected]> writes: > I'm going to call > > git push --mirror [email protected]:lilypond/lilypond.git > > to update the github mirror. However, this will cause the following > changes: > > > To github.com:lilypond/lilypond.git > - [deleted] refs/changes/31/482031/1 > - [deleted] refs/changes/31/482031/meta > - [deleted] refs/changes/32/482032/1
Huh, don't know what those are about: they seem specific to GitHub (or this repository). A mirror is a mirror: from that respect the push would not do damage, but any pull request or other magic that happened only at the GitHub site will be lost. So better wait at least a week for feedback before going ahead. Sounds annoying, but it would be a shame to lose work from somebody who thought contributing via GitHub the right way to proceed. -- David Kastrup
