git question

Mikolaj Konarski mikolaj at well-typed.com
Fri Oct 31 11:38:46 UTC 2014


> Right!  I'm on branch wip/new-flatten-skolems-Oct14, so
>         git push --force
> should push just that branch right?

Right. But don't trust me, try with --dry-run.

> 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?

The latter seems safest. Probably

    git push --force origin wip/new-flatten-skolems-Oct14

would work, depending on how your remotes are named.
Again, --dry-run. :)


More information about the ghc-devs mailing list