Re: GUB with local git-repo?

[Thomas Morley]

Phil, David,

thanks for the hints

Am Fr., 7. Juni 2019 um 13:40 Uhr schrieb David Kastrup <address@hidden>:
>
> 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.

Here I don't understand what you mean, could you explain more detailed?

> Can't you just clone a repository for which "origin" is
> your local repository rather than the official upstream?

Cheers,
  Harm