-w option;
authorwenzelm
Mon, 07 Jul 1997 09:07:08 +0200
changeset 3504 8493dbe2f009
parent 3503 390093b95cb0
child 3505 1cb4ea47d967
-w option;
lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Jul 07 09:06:26 1997 +0200
+++ b/lib/Tools/usedir	Mon Jul 07 09:07:08 1997 +0200
@@ -83,7 +83,7 @@
 if [ -n "$BUILD" ]; then
   exec $ISABELLE \
     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \
-    -q $LOGIC $NAME
+    -q -w $LOGIC $NAME
 else
   exec $ISABELLE \
     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \