Andres Freund <andres@anarazel.de> writes: > On 2017-01-03 13:02:28 -0500, Bruce Momjian wrote: >> Yeah, I was doing parallel pulls of different branches in git via shell >> script, and it seems the size of this commit showed me that doesn't >> work. Sorry.
> Shouldn't you check the results of something like this before pushing? > Sorry for piling on, but that seems like a quite critical step.
Actually, my takeaway from this was "don't ever use git reset on the repo". "git revert" would have been much safer. Yeah, it would have meant that git blame on the 9.2 branch would have some useless noise, but how much does anyone still care about that?
Possibly this time, but the generic answer is a lot harder.
If you do a git reset, you pay the one-time cost. Once the (fairly few) people who managed to pull in between have updated, the problem is gone.
If you do a git revert, the problem stays around forever (but it's a smaller one).
In the end it's going to be case-by-case. We may have done it wrong this time, but I don't think we can generally say what's right for the next one.
Except for like Andres says, always check *everything* before pushing. I know I always push with -n and then do a git show on that resulting set of commits just to make sure it's the one I want. It doesn't take a lot of extra time after each commit, and it easily finds things like this.