1-800-GIT-HELP (how to delete a user branch?)

[Gaius Mulley]

Jonathan Wakely <jwakely.gcc@gmail.com> writes:

> On Tue, 25 Oct 2022 at 13:23, Gaius Mulley via Gcc <gcc@gcc.gnu.org> wrote:
>>
>>
>> Just wondering what is the safest way to delete a user branch?
>>
>> [I used ./contrib/git-add-user-branch.sh and wanted to start over
>>  (user branch for m2 and gcc12)],
>
> When you say start over, do you mean reuse the same branch name for a
> different branch with unrelated history, but using the same name?

yes

> If yes, you can just force push the new history to the branch. That's
> the simplest answer.

great thanks a lot!  I will try this approach

> If you really want to delete the branch, then you just say:
>
> git push --dry-run --delete REMOTE BRANCH
> and if that looks right, remove the --dry-run option.
>
> The REMOTE will be something like users/gaius and BRANCH will be
> something like refs/users/gaius/heads/m2gcc12 depending on how you set
> up your local user branches.

many thanks useful info.