Re: How to force a push to succeed?

[Kevin Daudt <me@ikke.info>]

On Tue, Aug 22, 2017 at 05:55:25PM -0400, Jeffrey Walton wrote:
> I tested some changes that lead to a dead end. The changes need to be
> removed. The changes were added in 7 commits.
> 
> I went back in time to the point before the changes:
> 
>     $ git reset --hard HEAD~7
>     HEAD is now at 559fc3b Fix benchmark selection code (GH #464)
> 
> When I attempted to push:
> 
>     $ git push
>     Username for 'https://github.com': noloader
>     To https://github.com/noloader/cryptopp.git
>      ! [rejected]        master -> master (non-fast-forward)
> 
> I tried to commit, but Git claims there's nothing to add:
> 
>     $ git commit
>     On branch master
>     Your branch is behind 'origin/master' by 7 commits, and can be
> fast-forwarded.
> 
> Commit seems to be the wrong command as Git appears to be trying to do
> something I don't want.
> 
> How do I force the push to succeed?
> 
> Thanks in advance.

By actually doing a force push:

    git push --force-with-lease origin master

But note that this can interfere with others working on the same
repository, so be carefull when you use a force push.

Additionally, I can recommend using separate branches for things that
might turn up as dead ends (or even for every development). That way,
you can just throw away the branch if you want to discard it.

Hope this helps, Kevin.