diff --git a/doc/handbook/build-handbook.sh b/doc/handbook/build-handbook.sh index 98c5d2a8f..1689689be 100755 --- a/doc/handbook/build-handbook.sh +++ b/doc/handbook/build-handbook.sh @@ -1,11 +1,11 @@ #! /bin/sh -# this script build the eWoms handbook from its LaTeX sources. The +# this script builds the eWoms handbook from its LaTeX sources. The # result file is called "ewoms-handbook.pdf" -latex ewoms-handbook -bibtex ewoms-handbook -latex ewoms-handbook -latex ewoms-handbook -dvipdf ewoms-handbook +latex ewoms-handbook || exit $? +bibtex ewoms-handbook || exit $? +latex ewoms-handbook || exit $? +latex ewoms-handbook || exit $? +dvipdf ewoms-handbook || exit $? rm ewoms-handbook.dvi