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.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/63df28ca-464f-a209-5209-becaa8925dfd%40panix.com.
