lib/Tools/usedir
changeset 4075 8a467dc6e667
parent 3848 97bb3ff3c771
child 4419 950001e4859a
equal deleted inserted replaced
4074:3a2aa65288df 4075:8a467dc6e667
    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