It took me longer then I expected it to, to find out how to revert a single file using git. Git revert is not it, that’s for creating a commit to undo the changes of another commit. Maybe git reset? No, that resets the current HEAD, not a specific file, it would seem. Turns out it’s just a simple re-checkout of the offending file. D’oh.

git checkout ${offending_file}