diff options
| -rw-r--r-- | Doc/html/style.css | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index 762d1c4..5744630 100644 --- a/Doc/html/style.css +++ b/Doc/html/style.css @@ -67,9 +67,19 @@ div.warning { background-color: #fffaf0; margin-left: 2em; margin-right: 2em; } -div.warning .label { font-size: 110%; +div.warning .label { font-family: sans-serif; + font-size: 110%; margin-right: 0.5em; } +div.note { background-color: #fffaf0; + border: thin solid black; + padding: 0.5em; + margin-left: 2em; + margin-right: 2em; } + +div.note .label { margin-right: 0.5em; + font-family: sans-serif; } + .release-info { font-style: italic; } .titlegraphic { vertical-align: top; } |