--- 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