diff options
Diffstat (limited to 'Doc/tools')
| -rwxr-xr-x | Doc/tools/mkhtml.sh | 4 |
1 files changed, 4 insertions, 0 deletions
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 @@ 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 $? |