Re: push-access

[David Kastrup]

Thomas Morley <address@hidden> writes:

> To revert the unwanted merge I did:
>
> git reset --hard HEAD~20

HEAD~20?  Huh.

> To push:
>
> git fetch
> git rebase origin dev/handle-grace
> git push origin HEAD:staging
>
>
> Hope it's ok

Hard to argue with success.  As long as you check before pushing, it's
hard to mess up.  Git will refuse to push anything that is not direct
progress from the state in the repository, so the worst thing one can
generally do is to push some unintended merge commit or get unwanted
additional commits in.

One thing that's worth doing before pushing is

git commit --amend

and then putting

Issue xxxx:

at the start of the first line in the commit message.  That makes it
easier in case of problems to find the respective issue tracker.

-- 
David Kastrup