# HG changeset patch
# User wenzelm
# Date 953142648 -3600
# Node ID deb604b3d9a9cc3b9eac0ed9b90313aed5c693d9
# Parent  ae32be343647f56abf55c8c90ee1d779696d4054
## -D document;

diff -r ae32be343647 -r deb604b3d9a9 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"