Re: GUB with local git-repo?

[David Kastrup]

Thomas Morley <address@hidden> writes:

> Hi Phil,
>
> let's see, if I understand correctly:
>
> For a public branch, I'd checkout a local branch, say: dev/issue4943
> Then make it public with
>   git push origin dev/issue4943
> Further changes added to this branch with
>   git push dev/issue4943 HEAD:staging

What?  No, just continue with

    git push origin dev/issue4943

> Invoking GUB with
>   make LILYPOND_BRANCH=dev/issue4943 lilypond
>
> Though, I don't know how to delete said branch from the official repo,
> after all work is done.

git push origin :dev/issue4943

Basically, push an empty ref.

Seems a bit strange that one can only work through the official
repository.  Can't you just clone a repository for which "origin" is
your local repository rather than the official upstream?

-- 
David Kastrup