diff -r 124bb367dc0e -r 4ca0b6507ed5 lib/Tools/usedir --- a/lib/Tools/usedir Tue May 20 19:34:50 1997 +0200 +++ b/lib/Tools/usedir Tue May 20 19:57:12 1997 +0200 @@ -82,16 +82,10 @@ if [ -n "$BUILD" ]; then exec $ISABELLE \ - -e "make_html := $HTML;" \ - -e "set_session\"$SESSION\";" \ - -e "exit_use_dir\".\";" \ - -e "reset make_html;" \ + -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \ -q $LOGIC $NAME else exec $ISABELLE \ - -e "make_html := $HTML;" \ - -e "set_session\"$SESSION\";" \ - -e "exit_use_dir\"$NAME\"; quit();" \ - -e "reset make_html;" \ + -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \ -r -q $LOGIC fi