On Thursday, September 22, 2022 at 7:15:21 PM UTC+2 [email protected] wrote:
> 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. > Plus, there won't be many occurrences, so no need to have an abbreviated form. You're right. Benoît > 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/4813743f-bff9-429a-9d99-13484eff5aaen%40googlegroups.com.
