|
From: | Eli Zaretskii |
Subject: | Re: Accidentally pushed a branch |
Date: | Sun, 19 Jun 2022 09:02:38 +0300 |
> From: Yuan Fu <casouri@gmail.com> > Date: Sat, 18 Jun 2022 17:00:43 -0700 > > Errr I accidentally pushed to tree-sitter rather than feature/tree-sitter, > how can I delete that branch? Sorry for the fuzz. I used git push origin --delete tree-sitter to delete that branch.
[Prev in Thread] | Current Thread | [Next in Thread] |