git question

Daniel Trstenjak 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
> 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


More information about the ghc-devs mailing list