diff options
Diffstat (limited to 'doc/manual.css')
| -rw-r--r-- | doc/manual.css | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/manual.css b/doc/manual.css index 6d5a3f09..b158aea3 100644 --- a/doc/manual.css +++ b/doc/manual.css @@ -2,13 +2,16 @@ h3 code { font-family: inherit ; } -pre { - font-size: 105% ; +pre, code { + font-size: 12pt ; } span.apii { float: right ; font-family: inherit ; + font-style: normal ; + font-size: small ; + color: gray ; } p+h1, ul+h1 { |