# HG changeset patch
# User wenzelm
# Date 864151032 -7200
# Node ID 4ca0b6507ed5eb02f169289a87e81813f6702ef3
# Parent  124bb367dc0ebd2d9bdd76c1c1ef482ec5750ed7
tuned command line;

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