wikimedia/mediawiki-extensions-WikiEditor
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor synced 2024-11-28 02:00:34 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge "Use font-family: monospace, Courier"

Browse source
This commit is contained in:
jenkins-bot 2015-01-24 07:59:52 +00:00 committed by Gerrit Code Review
parent b7fbb3d6e2 342cebaba6
commit c9b6a851b4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
modules/jquery.wikiEditor.toolbar.css
View file

@ -253,7 +253,7 @@
vertical-align: top;
}
.wikiEditor-ui-toolbar .section-help .page-table td.cell-syntax {
font-family: monospace, "Courier New";
font-family: monospace, Courier;
}
.wikiEditor-ui-toolbar .section-help .page-table td.cell-syntax,
.wikiEditor-ui-toolbar .section-help .page-table td.cell-result {
@ -276,7 +276,7 @@
color: black;
text-decoration: none;
cursor: pointer;
font-family: monospace, "Courier New";
font-family: monospace, Courier;
font-size: 1.25em;
line-height: 1;
}