I generally agree with David's approch. I have only some minor remarks (see review comments in the PR). Especially the memorium for Norm is a good idea - it is worth to put it in a prominent place.
On Saturday, December 18, 2021 at 9:11:57 PM UTC+1 David A. Wheeler wrote: > 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/2f7e81b7-fb4e-4308-ac16-90148b13a3b4n%40googlegroups.com.
