equal
deleted
inserted
replaced
80 |
80 |
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;" \ |
85 -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\".\"; make_html := false;" \ |
86 -e "set_session\"$SESSION\";" \ |
|
87 -e "exit_use_dir\".\";" \ |
|
88 -e "reset make_html;" \ |
|
89 -q $LOGIC $NAME |
86 -q $LOGIC $NAME |
90 else |
87 else |
91 exec $ISABELLE \ |
88 exec $ISABELLE \ |
92 -e "make_html := $HTML;" \ |
89 -e "make_html := $HTML; set_session\"$SESSION\"; exit_use_dir\"$NAME\"; make_html := false; quit();" \ |
93 -e "set_session\"$SESSION\";" \ |
|
94 -e "exit_use_dir\"$NAME\"; quit();" \ |
|
95 -e "reset make_html;" \ |
|
96 -r -q $LOGIC |
90 -r -q $LOGIC |
97 fi |
91 fi |