diff --git a/collects/scribble/scribble.css b/collects/scribble/scribble.css
index a96c9d19..e77470a2 100644
--- a/collects/scribble/scribble.css
+++ b/collects/scribble/scribble.css
@@ -2,7 +2,7 @@
 /* CSS seems backward: List all the classes for which we want a
    particular font, so that the font can be changed in one place.  (It
    would be nicer to reference a font definition from all the places
-   that we want it.) 
+   that we want it.)
 
    As you read the rest of the file, remember to double-check here to
    see if any font is set. */
@@ -51,12 +51,12 @@ table td {
 /* ---------------------------------------- */
 /* Navigation */
 
-.navleft { 
+.navleft {
   position: relative;
   float: left;
   white-space: nowrap;
 }
-.navright { 
+.navright {
   position: relative;
   float: right;
   white-space: nowrap;
@@ -201,11 +201,11 @@ font-weight: bold;
   margin: 0.2em 0.2em 0.2em 0.2em;
 }
 
-.sepspace { 
+.sepspace {
   font-size: 40%;
 }
 
-.septitle { 
+.septitle {
   font-size: 70%;
 }
 
@@ -375,7 +375,7 @@ i {
   background-color: #E8E8FF;
 }
 
-.inlinetop{ 
+.inlinetop{
   display: inline;
   vertical-align: top;
 }
@@ -437,23 +437,15 @@ i {
   color: blue;
 }
 
-.techoutside {
-  text-decoration: underline;
-  color: #d0d0d0;
-}
+.techoutside       { text-decoration: underline; color: #d0d0d0; }
+.techoutside:hover { text-decoration: underline; color: blue; }
 
-.techoutside:hover {
-  text-decoration: underline;
-  color: blue;
-}
-
-.techinside {
-  color: black;
-}
-
-.techinside:hover {
-  color: blue;
-}
+/* .techinside:hover doesn't work with FF, .techinside:hover>
+   .techinside doesn't work with IE, so use both (and IE doesn't
+   work with inherit in the second one, so use blue directly) */
+.techinside                    { color: black; }
+.techinside:hover              { color: blue; }
+.techoutside:hover>.techinside { color: inherit; }
 
 .bibliography td {
   vertical-align: top;
@@ -464,7 +456,7 @@ i {
   margin-right: 0.3em;
 }
 
-.smaller{ 
+.smaller{
   font-size: 82%;
 }
 
@@ -474,7 +466,7 @@ i {
   font-size: 1px;
 }
 
-.compact li p { 
+.compact li p {
   margin: 0 0 0 0;
   padding: 0 0 0 0;
 }