t-* labels on github

Stream: mathlib4

[Thomas Murrills]

I noticed that the meta label changed to t-meta, and there are now t-* labels for different areas, such as t-euclidean-geometry and t-algebra.

I was just curious—what does the t stand for?

[Yaël Dillies]

topic

[Thomas Murrills]

Makes sense, thx! :) I suppose meta is the odd one out, since it's not a mathematical topic like the others, but it is still a topic (description of the code's content) nonetheless.

[Mario Carneiro]

not all mathlib topics are mathematical

[Yaël Dillies]

Yes, it's not topic in the mathematical sense but topic in the "who can I bother to review this" sense.

[Yury G. Kudryashov]

I copied these labels from mathlib3 (and renamed meta to match) .

[Yury G. Kudryashov]

@Scott Morrison Many of your github issues should be labeled with t-meta. Could you please do this?

[Scott Morrison]

Done!