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

Drop wgCodeEditorEnableCore, default on, pointless to disable

Browse source 
Change-Id: I637ac6cc92183dbf73b6bb39d487c6d4099657be
This commit is contained in:
James D. Forrester 2019-07-12 10:58:50 -07:00
parent fd3f2bd2e6
commit 988bc3c0b1
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
},

16
includes/CodeEditorHooks.php
View file

@ -8,16 +8,12 @@ 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 ) {
return 'css';
} elseif ( $model === CONTENT_MODEL_JSON ) {
return 'json';
}
if ( $model === CONTENT_MODEL_JAVASCRIPT ) {
return 'javascript';
} elseif ( $model === CONTENT_MODEL_CSS ) {
return 'css';
} elseif ( $model === CONTENT_MODEL_JSON ) {
return 'json';
}
// Give extensions a chance