| changeset 2812 | dfcd1b00f294 |
| parent 2808 | e8a224e41b9f |
| child 2849 | 01a536a6e4fb |
| 2811:27dd00d74e5a | 2812:dfcd1b00f294 |
|---|---|
76 -q $COPYDB $LOGIC $NAME |
76 -q $COPYDB $LOGIC $NAME |
77 else |
77 else |
78 exec $ISABELLE \ |
78 exec $ISABELLE \ |
79 -e "make_html := $ISABELLE_HTML;" \ |
79 -e "make_html := $ISABELLE_HTML;" \ |
80 -e "set_session\"$SESSION\";" \ |
80 -e "set_session\"$SESSION\";" \ |
81 -e "exit_use_dir\"$NAME\";" \ |
81 -e "exit_use_dir\"$NAME\"; quit();" \ |
82 -r -q $LOGIC |
82 -r -q $LOGIC |
83 fi |
83 fi |