Copy in the stylesheet after latex2html is done.
diff --git a/Doc/tools/mkhtml.sh b/Doc/tools/mkhtml.sh
index 940d934..e20d3bf 100755
--- a/Doc/tools/mkhtml.sh
+++ b/Doc/tools/mkhtml.sh
@@ -31,6 +31,10 @@
  ${1:+$@} \
  $srcdir/$part/$part.tex || exit $?
 
+# copy in the stylesheet
+echo "cp $srcdir/html/style.css $part/$part.css"
+cp $srcdir/html/style.css $part/$part.css || exit $?
+
 echo "(cd $part; $srcdir/tools/node2label.pl \*.html)"
 cd $part
 $srcdir/tools/node2label.pl *.html || exit $?