diff options
| -rw-r--r-- | Doc/html/style.css | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index 9b8ebf5..3f8b3e8 100644 --- a/Doc/html/style.css +++ b/Doc/html/style.css @@ -61,6 +61,15 @@ var { font-family: times, serif; font-family: avantgarde, sans-serif; font-size: 110%; } +div.warning { background-color: #fffaf0; + border: thin solid black; + padding: 0.5em; + margin-left: 2em; + margin-right: 2em; } + +div.warning .label { font-size: 110%; + margin-right: 0.5em; } + .release-info { font-style: italic; } .titlegraphic { vertical-align: top; } |