Actually fix bug #20706 - Next time I will read more carefully and test more thouroug...

diff --git a/includes/DefaultSettings.php b/includes/DefaultSettings.php
index 8429c81..5f20dea 100644 (file)
--- a/includes/DefaultSettings.php
+++ b/includes/DefaultSettings.php
@@ -1682,7 +1682,7 @@ $wgCacheEpoch = '20030516000000';
  * to ensure that client-side caches do not keep obsolete copies of global
  * styles.
  */
-$wgStyleVersion = '273';
+$wgStyleVersion = '274';
 
 
 # Server-side caching:

diff --git a/skins/vector/main-ltr.css b/skins/vector/main-ltr.css
index 373413a..5371a46 100644 (file)
--- a/skins/vector/main-ltr.css
+++ b/skins/vector/main-ltr.css
@@ -707,6 +707,9 @@ blockquote {
        font-family: Times, "Times New Roman", serif;
        font-style: italic;
 }*/
+pre, code, tt {
+       font-family: monospace, sans-serif;
+}
 code {
        background-color: #f9f9f9;
 }
@@ -715,7 +718,6 @@ pre {
        border: 1px dashed #2f6fab;
        color: black;
        background-color: #f9f9f9;
-       font-size: 1.25em;
        line-height: 1.1em;
 }
 ul {

diff --git a/skins/vector/main-rtl.css b/skins/vector/main-rtl.css
index 7c5aee2..856ec6b 100644 (file)
--- a/skins/vector/main-rtl.css
+++ b/skins/vector/main-rtl.css
@@ -707,6 +707,9 @@ blockquote {
        font-family: Times, "Times New Roman", serif;
        font-style: italic;
 }*/
+pre, code, tt {
+       font-family: monospace, sans-serif;
+}
 code {
        background-color: #f9f9f9;
 }
@@ -715,7 +718,6 @@ pre {
        border: 1px dashed #2f6fab;
        color: black;
        background-color: #f9f9f9;
-       font-size: 1.25em;
        line-height: 1.1em;
 }
 ul {