lib/Tools/mkdir

--- a/lib/Tools/mkdir	Wed Mar 15 18:50:14 2000 +0100
+++ b/lib/Tools/mkdir	Wed Mar 15 18:50:48 2000 +0100
@@ -123,7 +123,7 @@
     echo "SRC = \$(ISABELLE_HOME)/src"
     echo "OUT = \$(ISABELLE_OUTPUT)"
     echo "LOG = \$(OUT)/log"
-    echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi"
+    echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
     echo
     echo
     echo "## $NAME"