On Monday, April 19, 2021 at 12:52:06 AM UTC+2 [email protected] wrote: > I think such a page would fit best as an additional HTML page on the > metamath web site, which could be developed on github next to the other web > pages. (I don't have any particular suggestions for what to put on the page > at the moment but I'd be happy to review or extend it if someone wants to > take a shot at it.) > > Mario >
I agree. Also, this would give an opportunity to organize the metamath/set.mm github repository (see https://github.com/metamath/set.mm/issues/1887). Benoît -- 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/2b5a19fe-ba9b-4707-980a-aa399306244en%40googlegroups.com.
