This was pushed into /extensions/ on Git. I doubt that this is what we should go since we have /skins/ for MediaWiki. I write this knowing that the handling of this skin is closer to that of an extension than that one of the "classic" skins. Cheers
Location on Git
No, it is an extension (I moved the page back). The extension:
- Defines a ResourceLoader module 'ext.agora.base'
- which contains some CSS for new styles (.mw-ui-button to start)
- Conditionally sends this module to the browser pages depending on config variables,the current page's title, and/or the current page's wiki actions
This CSS is in addition to the user's current skin.
Ah, this was a misconception on my end. I thought this extension provides a distinct skin. Thank you for explaining the details and fluffing up the documentation. :) Cheers