lib/Tools/mkdir
changeset 15703 727ef1b8b3ee
parent 15574 b1d1b5bfc464
child 15717 541e50adfc73
--- a/lib/Tools/mkdir	Wed Apr 13 09:48:41 2005 +0200
+++ b/lib/Tools/mkdir	Wed Apr 13 18:34:22 2005 +0200
@@ -137,7 +137,7 @@
     echo "OUT = \$(ISABELLE_OUTPUT)"
     echo "LOG = \$(OUT)/log"
     echo
-    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d pdf  ## -D generated"
+    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
     echo
     echo
     echo "## $NAME"