# HG changeset patch
# User wenzelm
# Date 1003766176 -7200
# Node ID f5b7c69a5a574774314e5c6181ddde8ef314e503
# Parent  0f5ffa1497db0c862b42c6a7fe376ccd9ced254f
-D generated;

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"