fix link-hovering so <a name='...'> (no href attribute) doesn't get
the hovering background
diff --git a/Doc/html/style.css b/Doc/html/style.css
index 4a9549f..a77fab5 100644
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -39,7 +39,8 @@
background-color: #ffffff; }
a:active { color: #ff0000; }
-a[href]:hover { background-color: #bbeeff; }
+a:link:hover { background-color: #bbeeff; }
+a:visited:hover { background-color: #bbeeff; }
a:visited { color: #551a8b; }
a:link { color: #0000bb; }
@@ -97,12 +98,17 @@
.grammar { background-color: #99ccff;
margin-right: 0.5in;
padding: 0.05in; }
-.productions { background-color: #bbeeff; }
-.productions a:hover { background-color: #99ccff; }
-.productions table { vertical-align: baseline; }
.grammar-footer { padding: 0.05in;
font-size: 85%; }
+.productions { background-color: #bbeeff; }
+.productions a:active { color: #ff0000; }
+.productions a:link:hover { background-color: #99ccff; }
+.productions a:visited:hover { background-color: #99ccff; }
+.productions a:visited { color: #551a8b; }
+.productions a:link { color: #0000bb; }
+.productions table { vertical-align: baseline; }
+
.email { font-family: avantgarde, sans-serif; }
.mailheader { font-family: avantgarde, sans-serif; }
.mimetype { font-family: avantgarde, sans-serif; }