author | wenzelm |
Wed, 15 Mar 2000 18:50:48 +0100 | |
changeset 8475 | deb604b3d9a9 |
parent 8474 | ae32be343647 |
child 8476 | 07d3e6383822 |
lib/Tools/mkdir | file | annotate | diff | comparison | revisions |
--- 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"