lib/Tools/usedir
changeset 2812 dfcd1b00f294
parent 2808 e8a224e41b9f
child 2849 01a536a6e4fb
equal deleted inserted replaced
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