mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor
synced 2024-11-24 00:06:49 +00:00
ebe89e3c7d
Use the new extension.json attribute instead. Bug: T214211 Change-Id: I79c45c6923fd19f6f9f068492b3bd6548161dd04 Depends-On: I27ecebe27d7aaebe6d1317bc5eaea9cca368b45d |
||
---|---|---|
.. | ||
WikiEditorHooks.php |