In fact, that's not me who did this, so I can't be sure what exactly he
did. He had master and devel branches. He rebased devel onto master branch
and did `git push -f`. Supposedly, push.default was set to matching and
both branches were pushed. But now in the remote repository master is
that her/his local copy of that remote was behind and after the rebase
he had lost those commits relative to the true remote, so when he force
pushed his rebased branches the remote was rolled back.
Philip
[sorry for the top post]
- Original Message -
*From:* Yuri Kanivetsky
