There seems to be extremely little documentation on Wikimedia's GitHub project https://github.com/wikimedia ... I can only find https://www.mediawiki.org/wiki/Gerrit/GitHub which mostly says we mirror a bunch of stuff from gerrit. And I know we have continuous integration of some kind set up for some projects, but it doesn't seem to be well documented in a place I could find.
There are also some repos that are mirrors of gerrit, and other repos that are primary repos, and it's a bit unclear what's what. More importantly, when folks have repos that they've been running on GitHub already and want to move into the wikimedia project (rather than switch to gerrit), what's the procedure? I'm an admin/owner so I can manually import people's repos but I'm not sure whether I'm supposed to... :)
We also have a lot of admins, which I wonder is necessary: https://github.com/orgs/wikimedia/people?utf8=%E2%9C%93&query=role%3Aown... https://github.com/orgs/wikimedia/people?utf8=%E2%9C%93&query=role%3Aowner+ Do we do any security review / removal of old accounts, or have a procedure for adding new admins?
-- brion