Zulip Chat Archive

Stream: mathlib4

Topic: close branch

Alex Zhang (Jul 12 2021 at 20:05):

How can I close a branch created by myself?

Yakov Pechersky (Jul 12 2021 at 20:08):

What do you mean by close? Close a PR? Delete a branch? Switch from a branch to another branch?

Alex Zhang (Jul 12 2021 at 20:16):

Sorry for the confusion. I mean, delete a branch with no PR relevant to it.

Yakov Pechersky (Jul 12 2021 at 20:18):

git branch -d ...

Mario Carneiro (Jul 12 2021 at 20:25):

That will only delete the branch locally. If you want to delete a branch on the remote, you do git push origin :mybranch IIRC (please don't do this to branches with unmerged commits unless you are sure no one else has seen it or cares)

Last updated: Dec 20 2023 at 11:08 UTC