What is it needed for? If an extension needs to be disabled, it should be removed from LocalSettings. Otherwise, it's not only confusing but also shoots you in the foot when an extension is kinda disabled but also kinda continues to be executed.
Related Gerrit Patches:
|mediawiki/extensions/CodeMirror : master||Remove $wgCodeMirrorEnableFrontend|
I support this. It's tripped me a couple of times now. What's the reasoning behind the flag? Can the extension still do some stuff (which we haven't enabled but third parties might have) with the flag being false?