Anchors ("a" elements) used only for the name attribute should not

change color on hover, only those that are link sources (href
attributes).

diff --git a/Doc/html/style.css b/Doc/html/style.css
index 3f8b3e858d9d9e433da0474368bdb0d11428cd93..762d1c45c567640b753fbe586a56e623beb84054 100644 (file)
--- a/Doc/html/style.css
+++ b/Doc/html/style.css
@@ -39,7 +39,7 @@ body                    { color: #000000;
                           background-color: #ffffff; }
 
 a:active                { color: #ff0000; }
-a:hover                 { background-color: #bbeeff; }
+a[href]:hover           { background-color: #bbeeff; }
 a:visited               { color: #551a8b; }
 a:link                  { color: #0000bb; }