set_session renamed to add_session;
authorwenzelm
Mon, 03 Nov 1997 11:48:02 +0100
changeset 4075 8a467dc6e667
parent 4074 3a2aa65288df
child 4076 8315021bf7d6
set_session renamed to add_session;
lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Nov 03 11:46:42 1997 +0100
+++ b/lib/Tools/usedir	Mon Nov 03 11:48:02 1997 +0100
@@ -93,10 +93,10 @@
 
 if [ -n "$BUILD" ]; then
   exec $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_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\"; add_session\"$SESSION\"; exit_use_dir\".\"; make_html := false; make_graph := false;" \
     -q -w $LOGIC $NAME
 else
   exec $ISABELLE \
-    -e "make_html := $INFO; make_graph := $INFO; output_dir := \"$ISABELLE_BROWSER_INFO\"; home_path := \"$HOME\"; set_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\"; add_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; make_graph := false; quit();" \
     -r -q $LOGIC
 fi