I would not do a push -f, just commit a fix on top. With mirrors in play it may cause problems.
On Thu, 22 Aug 2019 at 12:34, Clebert Suconic <[email protected]> wrote: > > 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
