[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Accidentally pushed a branch
|
From: |
Yuan Fu |
|
Subject: |
Re: Accidentally pushed a branch |
|
Date: |
Sun, 19 Jun 2022 19:34:54 -0700 |
> On Jun 18, 2022, at 11:02 PM, Eli Zaretskii <eliz@gnu.org> wrote:
>
>> 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.
Thanks :-)
Yuan