diff options
| -rwxr-xr-x | Doc/tools/mkhowto.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Doc/tools/mkhowto.sh b/Doc/tools/mkhowto.sh index 0541c85bbd..6b6bb962c6 100755 --- a/Doc/tools/mkhowto.sh +++ b/Doc/tools/mkhowto.sh @@ -34,6 +34,7 @@ build_html() { build_dvi() { latex $1 || exit $? + latex $1 || exit $? if [ -f $1.idx ] ; then `dirname $0`/fix_hack $1.idx || exit $? makeindex $1.idx || exit $? |