diff options
| -rw-r--r-- | skins/standard/global.css | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/skins/standard/global.css b/skins/standard/global.css index 8a7d91067..cd5e489a3 100644 --- a/skins/standard/global.css +++ b/skins/standard/global.css @@ -32,7 +32,11 @@ body, td, th, input { font-family: Verdana, sans-serif; font-size: small; - } + } + /* monospace is much smaller than Verdana by default, so we make it a bit bigger. */ + pre, code, kbd { + font-size: medium; + } /* global (end) */ /* header (begin) */ |