Last modified: 2013-09-06 08:16:51 UTC
I just noticed a change in the font used on JS pages such as https://pt.wikipedia.org/wiki/MediaWiki:Common.js?action=edit&debug=1 https://fr.wikipedia.org/wiki/MediaWiki:Common.js?action=edit&debug=1 They are using "font-family: sans-serif" instead of the desired "font-family: monospace". It is still possible to see the old behavior on e.g. https://en.wikipedia.org/wiki/MediaWiki:Common.js?action=edit&debug=1 The three wikis above are running 1.22wmf15 (5241654) right now, and all of them have CodeEditor installed. I tested using Google Chrome 29.0.1547.65 and Firefox 23.0.
*** This bug has been marked as a duplicate of bug 53734 ***
(Well, at least I think it's that.)