New "collective" contributor ?

[Benoit]

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

[Mario Carneiro]

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 <benoit...@gmail.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/915cad86-4988-4f62-ba40-90f4ceed6716n%40googlegroups.com.

[Benoit]

On Thursday, September 22, 2022 at 7:15:21 PM UTC+2 di....@gmail.com 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