@import 'mediawiki.mixins'; .CodeMirror { line-height: 1.5em; padding: 0.1em; } .mw-codeMirror-classicToolbar { border: 1px solid #a2a9b1; // If WikiEditor is installed but disabled, the classic toolbar // will still get wrapped in wikiEditor-ui .wikiEditor-ui-text & { border: 0; } } .CodeMirror pre, .CodeMirror-lines { padding: 0; } .mw-editbutton-codemirror-on { .background-image-svg( 'images/old-cm-on.svg', 'images/old-cm-on.png' ); } .mw-editbutton-codemirror-off { .background-image-svg( 'images/old-cm-off.svg', 'images/old-cm-off.png' ); } .wikiEditor-ui-toolbar .tool-codemirror-on { .background-image-svg( 'images/cm-on.svg', 'images/cm-on.png' ); } .wikiEditor-ui-toolbar .tool-codemirror-off { .background-image-svg( 'images/cm-off.svg', 'images/cm-off.png' ); }