> 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
> or
>       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':

[push]
   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.


Greetings,
Daniel
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs

Reply via email to