On Wed, Jan 4, 2017 at 4:05 PM, Tom Lane <t...@sss.pgh.pa.us> wrote: > Andres Freund <and...@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. -- Magnus Hagander Me: http://www.hagander.net/ Work: http://www.redpill-linpro.com/
