Update to CSS from trunk revision 1.35.

diff --git a/Doc/html/style.css b/Doc/html/style.css
index c722db36badc59fab5221b2af7bf49738849768d..f585744702052502ca0dcb23375d3e00fac1b7cd 100644 (file)
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -49,7 +49,15 @@ h1, h2, h3, h4, h5, h6  { font-family: avantgarde, sans-serif;
 h1                      { font-size: 180%; }
 h2                      { font-size: 150%; }
 h3, h4                  { font-size: 120%; }
-code, tt                { font-family: lucida typewriter, lucidatypewriter,
+
+/* LaTeX2HTML insists on inserting <br> elements into headers which
+ * are marked with \label.  This little bit of CSS magic ensures that
+ * these elements don't cause spurious whitespace to be added.
+ */
+h1>br, h2>br, h3>br,
+h4>br, h5>br, h6>br     { display: none; }
+
+code, tt                { font-family: "lucida typewriter", lucidatypewriter,
                                        monospace; }
 var                     { font-family: times, serif;
                           font-style: italic;
@@ -64,7 +72,7 @@ var                     { font-family: times, serif;
 
 div.warning             { background-color: #fffaf0;
                           border: thin solid black;
-                          padding: 0.5em;
+                          padding: 1em;
                           margin-left: 2em;
                           margin-right: 2em; }
 
@@ -74,7 +82,7 @@ div.warning .label      { font-family: sans-serif;
 
 div.note                { background-color: #fffaf0;
                           border: thin solid black;
-                          padding: 0.5em;
+                          padding: 1em;
                           margin-left: 2em;
                           margin-right: 2em; }
 
@@ -86,7 +94,7 @@ div.note .label         { margin-right: 0.5em;
 .titlegraphic           { vertical-align: top; }
 
 .verbatim pre           { color: #00008b;
-                          font-family: lucida typewriter, lucidatypewriter,
+                          font-family: "lucida typewriter", lucidatypewriter,
                                        monospace;
                           font-size: 90%; }
 .verbatim               { margin-left: 2em; }
@@ -131,7 +139,7 @@ div.note .label         { margin-right: 0.5em;
  */
 .seealso                { background-color: #fffaf0;
                           border: thin solid black;
-                          padding: 4pt; }
+                          padding: 0pt 1em 4pt 1em; }
 
 .seealso .heading       { font-size: 110%; }
 
@@ -140,3 +148,11 @@ div.note .label         { margin-right: 0.5em;
  * the top of modules.
  */
 .availability .platform { font-weight: bold; }
+
+
+/*
+ * Some specialization for printed output.
+ */
+@media print {
+  .online-navigation    { display: none; }
+  }