Minor style change.

diff --git a/Doc/html/style.css b/Doc/html/style.css
index 64b527d3c785d736cd81548e62139434d5e219d9..5f502ddb1fcfd8d7862cfc7d40f1f76888985af1 100644 (file)
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -39,6 +39,7 @@ body                    { color: #000000;
                           background-color: #ffffff; }
 
 a:active                { color: #ff0000; }
+a:hover                 { background-color: #bbeeff; }
 a:visited               { color: #551a8b; }
 a:link                  { color: #0000bb; }
 
@@ -72,6 +73,7 @@ var                     { font-family: times, serif;
                           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%; }