What's the process to add a new label to github?
F-min_const_generics to track which issues are actually relevant there
ugh, I don't know that there's a process, but adding F- foo labels is a constant annoyance to me. I'll go add it :)
(I like the idea of f- labels, I just mean that it's annoying to have to go create one)
I .. suspect you have the privileges actually, but maybe not
I do, but I never have been explicitly allowed to do so :laughing:
The process has so far been "just add it", especially for