I've been using Git for a while and I'm fairly well-versed with it.
However, an issue came up at work yesterday that was a bear to resolve. I'd
like to know if anyone has any advice or if there's a preferred way to deal
One of the developers (new to Git) did something bizarre like merge an old
branch into a new one and then push it. As a result, a lot of files were
deleted or changed (back to older versions). No one initially noticed (we
have a CI server but it only runs at specific times because the builds take
a while). Other folks pulled and some additional commits were even pushed
to remote on top of that bad merge.
So, "fixing" the remote branch was pretty easy (I did a rebase and skipped
the bad commits), then did a forced push to get remote in sync with my
rebased version. Others could pull just fine. However (and you may see
what's coming), when they did a push, the bad merge was pushed back to
remote because others now had it in their local repos. We were able to
finally deal with it by having the other folks do a hard reset so their
local repo matched the "good" head revision on remote.
What I'd like to ask is: Did I handle this the right way? Is there a better
way to deal with this sort of situation? I realize that one really
shouldn't get into this situation in the first place, but if it nonetheless
happens, how do you recover? Any advice appreciated.