diff options
Diffstat (limited to 'Doc/html')
| -rw-r--r-- | Doc/html/style.css | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Doc/html/style.css b/Doc/html/style.css index 64b527d..5f502dd 100644 --- 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%; } |