Answer to "Why are my branches getting deleted when someone merges my pull request?"

Skip to first unread message

Jim Kingdon

Feb 6, 2022, 3:12:29 PMFeb 6
to Metamath
Just wanted to let people know that Mario and I changed one of the
github settings and so if you make a branch in the repository (as
opposed to your own fork), make a pull request for it, and then that
pull request gets merged, the branch will be automatically deleted. If
you were still doing something with that branch there is an "undelete"
option (although the normal workflow would be to make a new branch for
the next thing you want to work on).

There are more details at
and we can re-open that issue or change the setting back if this is
causing trouble, but I wanted to at least let people know that we
changed it.

Reply all
Reply to author
0 new messages