I did a mistake yesterday, and I pushed a commit I wasn't supposed to. It was a commit only intended to my box, it says "fix"
nothing too wrong with it, but it has some checkstyle errors. which I can fix with a later commit. but if I could push -f and remove it it would be better. So, we don't have a way to push -f? Any ideas? -- Clebert Suconic
