diff options
| -rw-r--r-- | Doc/html/style.css | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index 5744630..4a9549f 100644 --- a/Doc/html/style.css +++ b/Doc/html/style.css @@ -89,6 +89,10 @@ div.note .label { margin-right: 0.5em; monospace; font-size: 90%; } .verbatim { margin-left: 2em; } +.verbatim .footer { padding: 0.05in; + font-size: 85%; + background-color: #99ccff; + margin-right: 0.5in; } .grammar { background-color: #99ccff; margin-right: 0.5in; |