Re: Accidentally pushed a branch

[Phil Sainty]

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.