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