diff options
Diffstat (limited to 'Doc/html')
| -rw-r--r-- | Doc/html/style.css | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index 5f502dd..9b8ebf5 100644 --- a/Doc/html/style.css +++ b/Doc/html/style.css @@ -65,9 +65,11 @@ var { font-family: times, serif; .titlegraphic { vertical-align: top; } -.verbatim { color: #00008b; +.verbatim pre { color: #00008b; font-family: lucida typewriter, lucidatypewriter, - monospace; } + monospace; + font-size: 90%; } +.verbatim { margin-left: 2em; } .grammar { background-color: #99ccff; margin-right: 0.5in; |