# 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"