The README.md of the "set.mm" repo said almost nothing. So I significantly extended it in this proposed change: https://github.com/metamath/set.mm/pull/2373/files
Basically, I tried to provide helpful information so that if someone started at *that* page, they'd eventually find hopefully-useful information. I tried to briefly document what I *think* we mostly agreed on as the process for merging changes. If I got it wrong, please discuss. I think it's important to document *some* rule, so that everyone knows what the rules are. I also put in a brief memorium for Norm (at the end). --- David A. Wheeler -- 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/CCDCE4E6-73B1-4D0B-924C-B0FD67CF50DE%40dwheeler.com.
