Sounds good. To delete a remote branch:
git push origin --delete bug53929 More information is at https://stackoverflow.com/questions/2003505/how-do-i-delete-a-git-branch-locally-and-remotely On Fri, May 3, 2019 at 4:03 PM Thomas Schmitt <scdbac...@gmx.net> wrote: > Hi, > > in order to maximize the probability for a last-minute problem report, > i created a git branch "bug53929" and committed the proposed change. > > "Made CD-TEXT character set interpretation more tolerant towards bad > input. Reaction on savannah bug 53929." > > http://git.savannah.gnu.org/cgit/libcdio.git/commit/?h=bug53929&id=a11824fda1b550a65c57c132a6ad321cab87c2e7 > > If no contrary reasons arise over the weekend, i propose to merge it > and to tell me how to delete it without nuking the repo. > > > Have a nice day :) > > Thomas > > >
