lib/Tools/document
changeset 26979 c58778bdf146
parent 26908 25fb7241f32e
child 28500 4b79e5d3d0aa
equal deleted inserted replaced
26978:fd4b4ecf935e 26979:c58778bdf146
   136   if [ -f IsaMakefile ]; then
   136   if [ -f IsaMakefile ]; then
   137     "$ISATOOL" make "$OUTFORMAT"
   137     "$ISATOOL" make "$OUTFORMAT"
   138     RC="$?"
   138     RC="$?"
   139   elif [ "$OUTFORMAT" = pdf ]; then
   139   elif [ "$OUTFORMAT" = pdf ]; then
   140     pre_latex pdf && \
   140     pre_latex pdf && \
   141     "$ISATOOL" latex -o pdf && \
   141     "$ISATOOL" latex -o pdf
   142     RC="$?"
   142     RC="$?"
   143   else
   143   else
   144     pre_latex dvi && \
   144     pre_latex dvi && \
   145     "$ISATOOL" latex -o "$OUTFORMAT"
   145     "$ISATOOL" latex -o "$OUTFORMAT"
   146     RC="$?"
   146     RC="$?"