On Tue, May 14, 2013 at 1:57 AM, Moriel Schottlender
<moriel(a)gmail.com>wrote;wrote:
Are all (or most) extensions in Github under
https://github.com/wikimedia/with
a "mediawiki-extensions-" prefix? Can I use that as a general rule of
thumb?
Yes. They're mirrored automatically.
Also, you're probably thinking this already, but just in case, make sure
not to remove Gerrit checking when you remove GitHub checking. Always good
to have that as a backup on the chance we ever move away from GitHub.
Or set up some caching on Gitweb, so it's usable for this kind of thing.
Matt Flaschen