Add support for a --pdf option to cause a PDF file to be created instead;

most of the processing is the same and has to be done anyway.

Doc/tools/mkdvi.sh

@@ -7,20 +7,30 @@ cd `dirname $0`/..
 srcdir=`pwd`
 cd $WORKDIR
 
-PART=$1
+latex=latex
+if [ "$1" = "--pdf" ] ; then
+    pdf=true
+    latex=pdflatex
+    shift 1
+fi
 
-TEXINPUTS=$srcdir/$PART:$TEXINPUTS
+part=$1; shift 1
+
+TEXINPUTS=$srcdir/$part:$TEXINPUTS
 export TEXINPUTS
 
 set -x
-$srcdir/tools/newind.py >$PART.ind || exit $?
-latex $PART || exit $?
-if [ -f $PART.idx ] ; then
+$srcdir/tools/newind.py >$part.ind || exit $?
+$latex $part || exit $?
+if [ -f $part.idx ] ; then
     # using the index
-    $srcdir/tools/fix_hack $*.idx || exit $?
-    makeindex -s $srcdir/texinputs/myindex.ist $*.idx || exit $?
+    $srcdir/tools/fix_hack $part.idx || exit $?
+    makeindex -s $srcdir/texinputs/myindex.ist $part.idx || exit $?
 else
     # skipping the index; clean up the unused file
-    rm -f $PART.ind
+    rm -f $part.ind
 fi
-latex $PART || exit $?
+if [ "$pdf" ] ; then
+    $srcdir/tools/toc2bkm.py $part
+fi
+$latex $part || exit $?