> On Sep 20, 2021, at 11:55 AM, Brian Larson <[email protected]> wrote: > > My mistake: When editing set.mm, I inadvertently deleted the $t > I would still request that one $t comment be allowed per file, so my errors > would be confined to my .mm files rather than added latexdef commands to > set.mm.
Norm will ultimately decide if more than one $t is allowed. That said, once “more than one $t” is allowed, I recommend adding no more restrictions. if “more than 1” $t is allowed, just allow them. --- 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/42026263-0675-4416-87C0-011D755800F6%40dwheeler.com.
