tuned command line;
authorwenzelm
Tue, 20 May 1997 19:57:12 +0200
changeset 3264 4ca0b6507ed5
parent 3263 124bb367dc0e
child 3265 8358e19d0d4c
tuned command line;
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