.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;
}