reset make_html afterwards;
authorwenzelm
Tue, 20 May 1997 19:27:24 +0200
changeset 3254 9effaaf77303
parent 3253 ea75747190a7
child 3255 7678f3d93053
reset make_html afterwards;
lib/Tools/usedir
--- a/lib/Tools/usedir	Tue May 20 19:26:43 1997 +0200
+++ b/lib/Tools/usedir	Tue May 20 19:27:24 1997 +0200
@@ -85,11 +85,13 @@
     -e "make_html := $HTML;" \
     -e "set_session\"$SESSION\";" \
     -e "exit_use_dir\".\";" \
+    -e "reset make_html;" \
     -q $LOGIC $NAME
 else
   exec $ISABELLE \
     -e "make_html := $HTML;" \
     -e "set_session\"$SESSION\";" \
     -e "exit_use_dir\"$NAME\"; quit();" \
+    -e "reset make_html;" \
     -r -q $LOGIC
 fi