mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor
synced 2024-11-27 17:50:44 +00:00
933231e808
User-options related classes are being moved to the MediaWiki\User\Options namespace in MediaWiki Core; reflect that change here. Bug: T352284 Depends-On: I9822eb1553870b876d0b8a927e4e86c27d83bd52 Change-Id: Ia3e82b9271fd7d5ecc27e58f3f955c427f83346a |
||
---|---|---|
.. | ||
Hooks.php |