daniel.trstenjak at gmail.com
Fri Oct 31 11:37:14 UTC 2014
> Right! I'm on branch wip/new-flatten-skolems-Oct14, so
> git push --force
> should push just that branch right?
> If I want to be super-safe, and say "push only this branch" would I say
> git push --force HEAD
> git push --force wip/new-flatten-skolems-Oct14
> or something like that?
To ensure, that you're only operating on your current branch you can
add to your '~/.gitconfig':
default = simple
Newer versions of git have this now as their default behaviour, but
I'm not quite sure which git version was the first one.
More information about the ghc-devs