Finally commit the font changes that have been live on the development site
for a month or more.
diff --git a/Doc/html/style.css b/Doc/html/style.css
index b24998c..cfd5942 100644
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -47,11 +47,14 @@
h1 { font-size: 180%; }
h2 { font-size: 150%; }
h3, h4 { font-size: 120%; }
-code, tt { font-family: monospace; }
+code, tt { font-family: lucida typewriter, lucidatypewriter,
+ monospace; }
var { font-family: times, serif;
font-style: italic;
font-weight: normal; }
+.typelabel { font-family: lucida, sans serif; }
+
.navigation td { background-color: #99ccff;
font-weight: bold;
font-family: avantgarde, sans-serif;
@@ -61,7 +64,9 @@
.titlegraphic { vertical-align: top; }
-.verbatim { color: #00008b; }
+.verbatim { color: #00008b;
+ font-family: lucida typewriter, lucidatypewriter,
+ monospace; }
.grammar { background-color: #99ccff;
margin-right: 0.5in;