wikimedia/mediawiki-extensions-CodeEditor
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeEditor synced 2024-11-15 03:23:45 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge "Drop wgCodeEditorEnableCore, default on, pointless to disable"

Browse source
This commit is contained in:
jenkins-bot 2019-07-18 15:28:50 +00:00 committed by Gerrit Code Review
parent f312224037 988bc3c0b1
commit e09b486175
2 changed files with 6 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
extension.json
View file

@ -31,9 +31,6 @@
"i18n"
]
},
"config": {
"CodeEditorEnableCore": true
},
"DefaultUserOptions": {
"usecodeeditor": 1
},

4
includes/CodeEditorHooks.php
View file

@ -8,9 +8,6 @@ class CodeEditorHooks {
* @return null|string
*/
public static function getPageLanguage( Title $title, $model, $format ) {
global $wgCodeEditorEnableCore;
if ( $wgCodeEditorEnableCore ) {
if ( $model === CONTENT_MODEL_JAVASCRIPT ) {
return 'javascript';
} elseif ( $model === CONTENT_MODEL_CSS ) {
@ -18,7 +15,6 @@ class CodeEditorHooks {
} elseif ( $model === CONTENT_MODEL_JSON ) {
return 'json';
}
}
// Give extensions a chance
// Note: $model and $format were added around the time of MediaWiki 1.28.