mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeEditor
synced 2024-11-13 17:53:17 +00:00
51cd95fac9
Remove using of User:getOption since this method will be hard-deprecated. Now it is soft-deprecated Bug: T296083 Change-Id: Iae0c0cd3ab4ffdfd6cfce5e7ced81dfae3d4a359 |
||
---|---|---|
.. | ||
Hooks.php |