equal
  deleted
  inserted
  replaced
  
    
    
    91   | 
    91   | 
    92 [ -z "$SESSION" ] && SESSION=$(basename $NAME)  | 
    92 [ -z "$SESSION" ] && SESSION=$(basename $NAME)  | 
    93   | 
    93   | 
    94 if [ -n "$BUILD" ]; then  | 
    94 if [ -n "$BUILD" ]; then  | 
    95   exec $ISABELLE \  | 
    95   exec $ISABELLE \  | 
    96     -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;" \  | 
    96     -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;" \  | 
    97     -q -w $LOGIC $NAME  | 
    97     -q -w $LOGIC $NAME  | 
    98 else  | 
    98 else  | 
    99   exec $ISABELLE \  | 
    99   exec $ISABELLE \  | 
   100     -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();" \  | 
   100     -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();" \  | 
   101     -r -q $LOGIC  | 
   101     -r -q $LOGIC  | 
   102 fi  | 
   102 fi  |