# HG changeset patch
# User wenzelm
# Date 864149244 -7200
# Node ID 9effaaf773035df28b7219bd239ba241c39ecb03
# Parent  ea75747190a76a2288c0f6bbc8d204dc7fd6d576
reset make_html afterwards;

diff -r ea75747190a7 -r 9effaaf77303 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