Re: Accidentally pushed a branch

[Yuan Fu]

> On Jun 18, 2022, at 11:16 PM, Phil Sainty <psainty@orcon.net.nz> wrote:
> 
> On 2022-06-19 12:00, Yuan Fu wrote:
>> Errr I accidentally pushed to tree-sitter rather than
>> feature/tree-sitter, how can I delete that branch?
> 
> Eli has answered, but as a FYI:
> 
> There's a somewhat obtuse git syntax for deleting things, which
> is to say "push 'nothing' to <branch>" via the more-verbose push
> syntax "git push <remote> <from>:<to>"
> 
> Hence "git push origin :tree-sitter" would delete the tree-sitter
> branch on the origin remote, because the <from> value is empty.
> 
> This may help to make sense of the explanation of the --delete
> option in the git-push man page.

Thanks, TIL :-)

Yuan