Copy in the stylesheet after latex2html is done.

diff --git a/Doc/tools/mkhtml.sh b/Doc/tools/mkhtml.sh
index 940d934160aa997b625373cc4ef2b3f12afc0666..e20d3bf123e83985d8c4decf95fa736c842e9ae8 100755 (executable)
--- a/Doc/tools/mkhtml.sh
+++ b/Doc/tools/mkhtml.sh
@@ -31,6 +31,10 @@ latex2html \
  ${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 $?