tweak website style sheets (thanks to Robert Goldman!)

[cl-graph.git] / website / source / user-guide.css

diff --git a/website/source/user-guide.css b/website/source/user-guide.css
index a0c4162..2e83f90 100644 (file)
--- a/website/source/user-guide.css
+++ b/website/source/user-guide.css
@@ -125,11 +125,16 @@ h3, h4 {
 
 .documentation.header {
        display: block;
+       background-color: lightgrey;
+       color: black;
        position: relative;
-       border-top-style: solid;
-       border-top-width: 1pt;
        padding-top: 4px;
        margin-top: 2em;
+       width:auto;
+       min-width:120px;
+       font-size: medium;
+       padding: 1mm 1mm 1mm 1em;
+       border: none;
 }
 
 .documentation.contents {
@@ -141,7 +146,7 @@ h3, h4 {
        font-weight: bold;
        float: left;
        padding-right: 10px;
-       width: 125px;
+       width: 80%;
 }
 
 .documentation-kind {