On 12/24/2013 09:11 PM, Joaquin M Lopez Munoz wrote:
Bjørn Roald
writes: On 12/24/2013 06:17 PM, Bjørn Roald wrote:
right, see my reply to Peter on this, copy-paste error of mine. Should have been.
git reset --hard 3239677c40b6e15d1bb49675cabb077460333538
OK, I try again. git reset --hard 802543fd948b5cf41460addf2260693f08cf7f8d
Did that, merged from develop, resolved conflicts as theirs (develop's), commited OK but push failed with
git.exe push --progress "origin" master:master
To https://github.com/boostorg/multi_index.git ! [rejected] master -> master (non-fast-forward) error: failed to push some refs to 'https://github.com/boostorg/multi_index.git' hint: Updates were rejected because the tip of your current branch is behind hint: its remote counterpart. Integrate the remote changes (e.g. hint: 'git pull ...') before pushing again. hint: See the 'Note about fast-forwards' in 'git push --help' for details.
git did not exit cleanly (exit code 1) (13510 ms @ 24/12/2013 21:09:27)
It tells you that you try to do a non-trivial merge at the remote repository, and refuses to do so without some more assertion from you that that is what you want. git push --force or git push -f should do it, just use gitk or other tool to make sure the master you have locally is what you want first. That should take care of what you desire, But you should then be worried the bad merge commit may already be referenced by somebody, and you would be subject for some heat if you break canonical boost clone or submodule update as your bad commit is not available. That may happen if git garbage collection cleans up on the remote and find nothing referencing your old commit any longer. To prevent this you must make sure some git ref on https://github.com/boostorg/multi_index/ reference the bad commit. You may then push your tag for the bad merge commit if you like to. If you made the tag I suggested, do git push --tags done. In TG i think there is a checkbox for tags in the push dialog. You can alternatively use a branch with a obvious not to use name for this, e.g. git checkout -b trash/bad-master-merges 3239677c4 git push or if you made the tag as I suggested, git checkout -b trash/bad-master-merges bad-merge git push git tag -d bad-merge # to remove the tag from local repository A branch may be simpler to clean up in future if you like to. -- Bjørn