mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeEditor
synced 2024-11-24 07:13:27 +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
5 lines
540 B
XML
5 lines
540 B
XML