Mirror of https://gerrit.wikimedia.org/g/mediawiki/extensions/CodeMirror

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
.phan	Add phan	2019-04-09 20:35:56 +02:00
i18n	Localisation updates from https://translatewiki.net.	2020-02-26 08:24:34 +01:00
includes	Move check for 'usebetatoolbar' from JS to PHP	2020-02-23 20:50:17 +00:00
resources	Unify monospace font stack. Avoid potential sizing bug caused by weird browser behavior with font-family: monospace;	2020-02-28 04:44:07 +00:00
tests/phpunit	Restore GetPreferences hook handler registration	2018-07-03 14:25:01 -07:00
.eslintrc.json	build: Update linters	2019-11-15 16:20:25 +00:00
.gitignore	build: Update eslint-config-wikimedia to 0.11.0	2019-03-06 12:10:29 +00:00
.gitreview	Whoops, track not trace	2016-10-24 17:02:17 -07:00
.phpcs.xml	Remove @staticvar doc annotation	2018-09-09 20:04:35 +02:00
.stylelintrc.json	Use json extension for .stylelintrc	2017-08-19 09:40:58 +02:00
CODE_OF_CONDUCT.md	build: Updating mediawiki/phan-taint-check-plugin to 1.3.0	2018-08-19 10:46:12 +00:00
composer.json	build: Updating composer dependencies	2020-01-29 02:08:53 +00:00
extension.json	Unify monospace font stack. Avoid potential sizing bug caused by weird browser behavior with font-family: monospace;	2020-02-28 04:44:07 +00:00
Gruntfile.js	build: Update linters	2019-11-15 16:20:25 +00:00
package-lock.json	build: Updating npm dependencies	2020-02-20 20:23:19 +00:00
package.json	build: Updating npm dependencies	2020-02-20 20:23:19 +00:00