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