Remove styling information that conflicts with or duplicates the stylesheet;
different browsers resolve the conflicts differently, and the "proper"
resolution is not what we actually want.
Reported by Peter Funk <pf@artcom-gmbh.de>.
diff --git a/Doc/tools/mkmodindex b/Doc/tools/mkmodindex
index 45c7485..1c22c43 100755
--- a/Doc/tools/mkmodindex
+++ b/Doc/tools/mkmodindex
@@ -173,8 +173,7 @@
src="%(iconserver)s/%(uplinkicon)s.%(imgtype)s"></a></td>
<td><img width="32" height="32" align="bottom" border="0" alt=""
src="%(iconserver)s/blank.%(imgtype)s"></td>
-<td align="center" bgcolor="#99CCFF" width="100%%">
- <b class="title">%(title)s</b></td>
+<td align="center" width="100%%">%(title)s</td>
<td><img width="32" height="32" align="bottom" border="0" alt=""
src="%(iconserver)s/blank.%(imgtype)s"></td>
<td><img width="32" height="32" align="bottom" border="0" alt=""
@@ -196,7 +195,7 @@
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<link rel="STYLESHEET" href="lib/lib.css">
</head>
-<body bgcolor=white>
+<body>
''' + NAVIGATION + '''\
<hr>