lib/Tools/mkdir
changeset 8475 deb604b3d9a9
parent 8289 5b288a96bc61
child 8488 58e37d59c146
     1.1 --- a/lib/Tools/mkdir	Wed Mar 15 18:50:14 2000 +0100
     1.2 +++ b/lib/Tools/mkdir	Wed Mar 15 18:50:48 2000 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4      echo "SRC = \$(ISABELLE_HOME)/src"
     1.5      echo "OUT = \$(ISABELLE_OUTPUT)"
     1.6      echo "LOG = \$(OUT)/log"
     1.7 -    echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi"
     1.8 +    echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
     1.9      echo
    1.10      echo
    1.11      echo "## $NAME"