Ok, I'll take this today or tomorrow. On Wednesday, November 23, 2022 at 3:55:32 PM UTC+1 [email protected] wrote:
> Can I get a review on https://github.com/metamath/set.mm/pull/2927 ? > There's a moderately detailed comment there describing what this is > about, but please do ask if you still have questions. It is quite > similar to recently merged pull requests. > > (And while I'm at it https://github.com/metamath/set.mm/pull/2929 and > https://github.com/metamath/metamath-exe/pull/106 are small > documentation fixes ready for review). > > > -- 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/4441947a-d7c9-4c82-b074-5d68964093f4n%40googlegroups.com.
