author | wenzelm |
Mon, 07 Jul 1997 09:07:08 +0200 | |
changeset 3504 | 8493dbe2f009 |
parent 3503 | 390093b95cb0 |
child 3505 | 1cb4ea47d967 |
lib/Tools/usedir | file | annotate | diff | comparison | revisions |
--- 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();" \