Thomas Morley <[email protected]> writes: > To revert the unwanted merge I did: > > git reset --hard HEAD~20
HEAD~20? Huh. > To push: > > git fetch > git rebase origin dev/handle-grace > git push origin HEAD:staging > > > Hope it's ok Hard to argue with success. As long as you check before pushing, it's hard to mess up. Git will refuse to push anything that is not direct progress from the state in the repository, so the worst thing one can generally do is to push some unintended merge commit or get unwanted additional commits in. One thing that's worth doing before pushing is git commit --amend and then putting Issue xxxx: at the start of the first line in the commit message. That makes it easier in case of problems to find the respective issue tracker. -- David Kastrup _______________________________________________ lilypond-devel mailing list [email protected] https://lists.gnu.org/mailman/listinfo/lilypond-devel
