mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeEditor
synced 2024-11-30 18:04:27 +00:00
Don't use deprecated mediawiki.api.options
It was merged into `mediawiki.api`. Bug: T196802 Change-Id: I03dad49e2b7949ad539d405d2dff933b288eec98
This commit is contained in:
parent
c28d0a5be3
commit
4f7fa3002a
|
@ -10,7 +10,7 @@
|
||||||
"license-name": "GPL-2.0-or-later AND BSD-3-Clause",
|
"license-name": "GPL-2.0-or-later AND BSD-3-Clause",
|
||||||
"type": "editor",
|
"type": "editor",
|
||||||
"requires": {
|
"requires": {
|
||||||
"MediaWiki": ">= 1.29.0",
|
"MediaWiki": ">= 1.32.0",
|
||||||
"extensions": {
|
"extensions": {
|
||||||
"WikiEditor": "*"
|
"WikiEditor": "*"
|
||||||
}
|
}
|
||||||
|
@ -53,7 +53,6 @@
|
||||||
"ext.codeEditor.ace",
|
"ext.codeEditor.ace",
|
||||||
"jquery.ui.resizable",
|
"jquery.ui.resizable",
|
||||||
"mediawiki.api",
|
"mediawiki.api",
|
||||||
"mediawiki.api.options",
|
|
||||||
"mediawiki.user",
|
"mediawiki.user",
|
||||||
"user.options",
|
"user.options",
|
||||||
"mediawiki.cookie",
|
"mediawiki.cookie",
|
||||||
|
|
Loading…
Reference in a new issue