I don't think it needs to use initials; that would only matter for putting in the contributor list and it should not be in there. (Contributed by the Metamath team, 22-Sep-2022.) parses just fine as a contribution comment.
On Thu, Sep 22, 2022 at 1:11 PM Benoit <[email protected]> wrote: > Some statements were collectively written/thought, for instance the > ~conventions-* statements. I think we could create a contributor "The > Metamath team", initials "MM", for the contribution tag of these > statements. What do you think ? > > 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/915cad86-4988-4f62-ba40-90f4ceed6716n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/915cad86-4988-4f62-ba40-90f4ceed6716n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSu6%2B_uj6LynqzzfvL%3D5BvN-gmu%3DD0kcCaznME5qj03ieg%40mail.gmail.com.
