diff -r 0f5ffa1497db -r f5b7c69a5a57 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Mon Oct 22 14:58:05 2001 +0200
+++ b/lib/Tools/mkdir	Mon Oct 22 17:56:16 2001 +0200
@@ -138,7 +138,7 @@
     echo "OUT = \$(ISABELLE_OUTPUT)"
     echo "LOG = \$(OUT)/log"
     echo
-    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi  ## -D document"
+    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi  ## -D generated"
     echo
     echo
     echo "## $NAME"