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