delete remote branch
jan.stolarek at p.lodz.pl
Thu Sep 12 09:06:01 UTC 2013
> Not rebasing my branches is a terrible choice. The other options
> are to either never push my branches, or to push my branches somewhere
> other than to the main repo, e.g., github.
One more choice is to create a new branch with -vX appended to the name (where X is version number), rebase it on top of master and push that rebased branch:
git checkout my-branch-v1
git checkout -b my-branch-v2
git rebase master
git push -u origin my-branch-v2
This workflow has a nice property of avoiding upstream rebasing, which is kinda important if you're not the only person working on a branch (man git-rebase, section RECOVERING FROM UPSTREAM REBASE gives a good description of the problem, if someone is interested). Of course at some point you will probably want to delete older branches, so this doesn't avoid the problem of privilages. Nor does it address the problem of resending commit messages to the list.
BTW. Why do consider storing code on github to be undesirable? I find github to be much more reliable (in terms of uptime) than our servers + I can do whatever I want with the branches (e.g. I don't store tens of branches from the main repo, just mine branches).
More information about the ghc-devs