apparently, if you know the right repository and alias, you can ping 400k people on GitHub: https://github.com/EpicGames/Signup/pull/24
food for thought as Coq maintainer teams grow.
the obvious fix, that some aliases/
@names are privileged, is apparently not implemented yet. But I guess it will be if those PR comments keep cropping up...
Will the world be a better place when half a million people are Coq maintainers?
more realistically, we might have a couple of hundred people maintaining Coq Platform projects...
These team aliases are supposed to be privileged. At least, I've seen people not being able to use them in the past. It could be the case that this person was actually an org member at the time when they used it (and was kicked out since).
Last updated: Dec 07 2023 at 17:01 UTC