diff options
Diffstat (limited to 'Doc')
| -rw-r--r-- | Doc/html/style.css | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index eae3307..3655666 100644 --- a/Doc/html/style.css +++ b/Doc/html/style.css @@ -10,7 +10,13 @@ .boldmath { font-family: "Century Schoolbook", serif; font-weight: bold } -/* Implement both fixed-size and relative sizes: */ +/* + * Implement both fixed-size and relative sizes. + * + * I think these can be safely removed, as it doesn't appear that + * LaTeX2HTML ever generates these, even though these are carried + * over from the LaTeX2HTML stylesheet. + */ small.xtiny { font-size : xx-small; } small.tiny { font-size : x-small; } small.scriptsize { font-size : smaller; } @@ -57,6 +63,14 @@ var { font-family: times, serif; .verbatim { color: #00008b; } +.grammar { background-color: #99ccff; + margin-right: 0.5in; + padding: 0.05in; } +.productions { background-color: #bbeeff; } +.productions table { vertical-align: baseline; } +.grammar-footer { padding: 0.05in; + font-size: 85%; } + .email { font-family: avantgarde, sans-serif; } .mimetype { font-family: avantgarde, sans-serif; } .newsgroup { font-family: avantgarde, sans-serif; } |