lib/Tools/usedir
changeset 3504 8493dbe2f009
parent 3264 4ca0b6507ed5
child 3636 3f2e55e5bacc
equal deleted inserted replaced
3503:390093b95cb0 3504:8493dbe2f009
    81 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
    81 [ -z "$SESSION" ] && SESSION=$(basename $NAME)
    82 
    82 
    83 if [ -n "$BUILD" ]; then
    83 if [ -n "$BUILD" ]; then
    84   exec $ISABELLE \
    84   exec $ISABELLE \
    85     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \
    85     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \
    86     -q $LOGIC $NAME
    86     -q -w $LOGIC $NAME
    87 else
    87 else
    88   exec $ISABELLE \
    88   exec $ISABELLE \
    89     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \
    89     -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \
    90     -r -q $LOGIC
    90     -r -q $LOGIC
    91 fi
    91 fi