>> As far as I can see, github's ticketing system doesn't allow to
>> simply update the patch; instead, you have to open a new ticket.
>
> Not true at all. Rebase your branch, then,
>
> git push -f origin my-branch
>
> ... will overwrite the contents of the pull request branch, and so
> update the request itself. I've done it many times. :-)
Good to know, thanks. [I assume that `overwrite' still somehow
retains the previously version for reference, right?]
Werner
_______________________________________________
lilypond-devel mailing list
lilypond-devel@gnu.org
https://lists.gnu.org/mailman/listinfo/lilypond-devel
