delete remote branch

Geoffrey Mainland mainland at
Thu Sep 12 12:43:17 UTC 2013

On 09/12/2013 05:06 AM, Jan Stolarek wrote:
>> 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.

Yes, it's not clear that this is a better approach. I'm only rebasing
branches for which I am the sole author. I believe Simon M. used a
workflow similar to mine for the new codegen branch at one point.

> 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).

For someone who is as busy as Simon PJ, it's easier to provide a branch
in the repo he's already using rather than force him to add yet another
remote just to have a look. Especially now that I am now also remote :(
I have nothing against github :)


More information about the ghc-devs mailing list