Jonathan Wakely <jwakely....@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.
