I think we should standardise on the capitalisation of
WG in our GitHub group names. They aren't all the same right now.
can you use all lowercase?
wg-mir-opt is lowercase while
WG-compiler-nll is uppercase.
Most of them are lowercase so we should probably match that.
We've also moved away from having a
WG-compiler- prefix to just
WG- in our Zulip groups, but unsure if that makes sense for GitHub.
The inconsistency in general with GitHub group names - which case, do they have descriptions, etc - bothers me slightly, but that's another topic. :stuck_out_tongue:
we're going to have to fix it when we migrate github teams to the team repo :D
(we should probably take advantage of GitHub child teams for working groups too, I just noticed them - it appears as if members of the child group needn't be members of the parent group)
@davidtwco I feel like GH child teams are not good for our purposes
if I recall, if you are a member of the child, you are also a member of the parent
i.e., it's more of a "subtype"-like relationship
which is the inverse of what we wanted
but I could be wrong
I don't think that is the case - in this documentation they have a screen showing more child team members than parent team members and say:
Members of a child team are not direct members of the parent team.
Well, that's true, but it also says
Child teams inherit the parent's access permissions, simplifying permissions management for large groups. Members of child teams also receive notifications when the parent team is @mentioned, simplifying communication with multiple groups of people.
and gives an example like
my point is that if we made "working groups" part of "t-compiler", then wg members would have the full rights of t-compiler.
it seems like we would need a setup more like
Fair enough, I misread the documentation there.