Nasty hack to add a --numeric parameter to skip the use of "logical"

names.

diff --git a/Doc/tools/mkhtml.sh b/Doc/tools/mkhtml.sh
index e20d3bf123e83985d8c4decf95fa736c842e9ae8..8857ef835bbd645a7c3739c8f002c6ad010ba40b 100755 (executable)
--- a/Doc/tools/mkhtml.sh
+++ b/Doc/tools/mkhtml.sh
@@ -13,6 +13,13 @@ cd `dirname $0`/..
 srcdir=`pwd`
 cd $WORKDIR
 
+use_logical_names=true
+
+if [ "$1" = "--numeric" ] ; then
+    use_logical_names=''
+    shift 1
+fi
+
 part=$1; shift 1
 
 TEXINPUTS=$srcdir/$part:$TEXINPUTS
@@ -35,6 +42,10 @@ latex2html \
 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 $?
+if [ "$use_logical_names" ] ; then
+    echo "(cd $part; $srcdir/tools/node2label.pl \*.html)"
+    cd $part
+    $srcdir/tools/node2label.pl *.html || exit $?
+else
+    echo "Skipping use of logical file names due to --numeric."
+fi