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 |