author | wenzelm |
Tue, 20 May 1997 19:27:24 +0200 | |
changeset 3254 | 9effaaf77303 |
parent 3253 | ea75747190a7 |
child 3255 | 7678f3d93053 |
lib/Tools/usedir | file | annotate | diff | comparison | revisions |
--- 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