# HG changeset patch # User wenzelm # Date 878554082 -3600 # Node ID 8a467dc6e667fd2e922fe2ce6fe9d2a32e2cc362 # Parent 3a2aa65288df461b55e99cd33a6d066416fc3842 set_session renamed to add_session; diff -r 3a2aa65288df -r 8a467dc6e667 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