# HG changeset patch
# User wenzelm
# Date 1003601815 -7200
# Node ID 2ce611f870e090b64d90d84228934bc34c508c17
# Parent  6d9d2b1d455dfd01efe516a74114154d9c174e6e
option -q also excludes -v true in generated stuff;
tuned message;

diff -r 6d9d2b1d455d -r 2ce611f870e0 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Sat Oct 20 20:15:44 2001 +0200
+++ b/lib/Tools/mkdir	Sat Oct 20 20:16:55 2001 +0200
@@ -96,6 +96,8 @@
 cd "$DIR"
 
 DOCUMENT_ROOT=""
+VERBOSE=""
+[ -z "$QUIET" ] && VERBOSE="-v true "
 
 if [ -n "$BUILD" ]; then
   IMAGES="$NAME"
@@ -136,7 +138,7 @@
     echo "OUT = \$(ISABELLE_OUTPUT)"
     echo "LOG = \$(OUT)/log"
     echo
-    echo "USEDIR = \$(ISATOOL) usedir -v true -i true -d dvi  ## -D document"
+    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi  ## -D document"
     echo
     echo
     echo "## $NAME"
@@ -266,9 +268,9 @@
 
   * $DIR/IsaMakefile contains compilation options and file dependencies
 
-  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
+  * $PREFIX/document/root.tex contains the LaTeX master document setup
 
-  * $PREFIX/document/root.tex contains the LaTeX master document setup
+  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
 
 EOF
 fi