On Sun, Nov 28, 2021 at 05:21:41PM +0100, Uwe Brauer wrote:
[...]
> Here is what I did finally and checked also the repository via the
> browser and all is well:
>
> git push -f origin c945bf50251150e0d4ad7ee751c7e9615cb4b3e8:master
> git branch -rD origin/copyright
> git branch -rD origin/copy
> git push origin :copy :copyright
Well, this is some advanced Git; glad you've sorted it out!
Still, unfortunately the premises I was basing my guidelines on - that you
actually want to _keep_ those commits and the branches other than master -
were wrong, as we've found out in another part of this thread. (Well, actually
I do not regret my advice because that was the safest default.)
Hence had I guessed better, the sequence would be way simpler and would
involve hard resetting one of the branches - as you've correctly found on SO:
git checkout master
git reset --hard c945bf502
^ would throw away the unneeded commits from the tip of the history line
git push -f origin master :copy :copyright
^ would force-update the master branch and delete - push nothing to -
the unneeded branches.
git remote prune origin
^ would make sure you have no remote branches not matching existing
branches on origin.
--
You received this message because you are subscribed to the Google Groups "Git
for human beings" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to git-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/git-users/20211129180118.fnkxfglxy27v4qvt%40carbon.
