mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeEditor
synced 2024-11-15 11:30:52 +00:00
b5312f1d4c
* Use resource loader embedding for better performance (uses a slightly hacky method to achieve this, the only alternative would be to fix the WikiEditor API, but that would introduce a version dependency) * Use SVGs from OOUI where available or create new ones where not. These are used and available under the OOjs UI MIT licence. * Provide PNG fallbacks using LESS mixin * Remove unused icons Change-Id: If38d51d24958716e2617c4cb515e7c0575cdfeba
9 lines
461 B
XML
9 lines
461 B
XML