# HG changeset patch
# User wenzelm
# Date 897664053 -7200
# Node ID 8e43dab90429d0a252e2a4995d52f5da23f0279a
# Parent  06f03dc5a1dce7034878f5a1e7b73479fe593330
Context.add_session;

diff -r 06f03dc5a1dc -r 8e43dab90429 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Jun 12 17:06:58 1998 +0200
+++ b/lib/Tools/usedir	Fri Jun 12 17:07:33 1998 +0200
@@ -112,7 +112,7 @@
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
+    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
     -q -w $LOGIC $NAME > $LOG 2>&1
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
@@ -120,7 +120,7 @@
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
+    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; Context.add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
     -r -q $LOGIC > $LOG 2>&1
 fi