Ooops, Repointing Git Head
I screwed up. I force pushed a branch but I forgot to tell git which branch to push so it clobbered another branch.
Drat, since I hadn’t updated develop in a few hours there were a bunch of changes in it that I just killed. Fortunately I know that git is really just a glorified linked list and that nothing is ever deleted. I just needed to update where the head pointer was pointing. I grabbed the SHA of the latest develop commit from the build server knowing that it was late at night and nobody else was likely to have snuck a commit into develop that the server missed.
Then I just force updated my local develop and pushed it back up
All was good again.