diff -r 2677db44c795 -r 727ef1b8b3ee lib/Tools/mkdir
--- 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"