mediawiki-extensions-CodeMi.../resources/lib/codemirror-fixes.less
AronDemian d70bd9d1ae Unify monospace font stack. Avoid potential sizing bug caused by weird browser behavior with font-family: monospace;
Problem: browsers implicitly and unexpectedly set the font-size to something around 13px with `font-family: monospace;`, but not with `font-family: monospace,monospace;`.
See:  http://code.iamkate.com/html-and-css/fixing-browsers-broken-monospace-font-handling/

Bug: T176636
Change-Id: Ied24a0cde7db4a6092d2cd7a6207d0a361424c3f
Related: T245568
Related: T245476
2020-02-28 04:44:07 +00:00

7 lines
272 B
Plaintext

.CodeMirror {
// Fix `font-family: monospace;` caused weird font sizing of browsers.
// Task: https://phabricator.wikimedia.org/T176636
// See: http://code.iamkate.com/html-and-css/fixing-browsers-broken-monospace-font-handling/
font-family: monospace, monospace;
}