On Monday, February 13, 2023 at 7:20:03 PM UTC+1 David A. Wheeler wrote: All: I'm thinking it might be a good idea to create a new "database area", "mpetxt" (to match "mpeuni"/"mpegif"), with many simple text files - 1 per proof.
So your idea is to replace the term "mpeascii" from https://groups.google.com/g/metamath/c/_c3viH80_w8/m/i1PQSRJJBAAJ with "mpetxt"? I'm fine with that. 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/fd1697ba-0fe0-4b45-bf26-5fc14624cc85n%40googlegroups.com.
