## -D document;
authorwenzelm
Wed, 15 Mar 2000 18:50:48 +0100
changeset 8475 deb604b3d9a9
parent 8474 ae32be343647
child 8476 07d3e6383822
## -D document;
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"