Answer to "Why are my branches getting deleted when someone merges my pull request?"
25 views
Skip to first unread message
Jim Kingdon
Feb 6, 2022, 3:12:29 PM2/6/22
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 set.mm 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 https://github.com/metamath/set.mm/issues/2476
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.
github settings and so if you make a branch in the set.mm 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 https://github.com/metamath/set.mm/issues/2476
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
Forward
0 new messages