# HG changeset patch
# User wenzelm
# Date 858705652 -3600
# Node ID dfcd1b00f29421646b89f799eb3d0848fddb3922
# Parent  27dd00d74e5acfc837a7ce1a315ca1f6653dfeb4
added quit();

diff -r 27dd00d74e5a -r dfcd1b00f294 lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Mar 18 18:20:26 1997 +0100
+++ b/lib/Tools/usedir	Tue Mar 18 18:20:52 1997 +0100
@@ -78,6 +78,6 @@
   exec $ISABELLE \
     -e "make_html := $ISABELLE_HTML;" \
     -e "set_session\"$SESSION\";" \
-    -e "exit_use_dir\"$NAME\";" \
+    -e "exit_use_dir\"$NAME\"; quit();" \
     -r -q $LOGIC
 fi