lib/Tools/document
changeset 7814 ef6d84f16592
parent 7793 e0676a932348
child 7857 a49a3978fe3a
     1.1 --- a/lib/Tools/document	Sat Oct 09 23:15:40 1999 +0200
     1.2 +++ b/lib/Tools/document	Sat Oct 09 23:16:31 1999 +0200
     1.3 @@ -60,23 +60,49 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -#prepare document
     1.8 +# check format
     1.9 +
    1.10 +case "$OUTFORMAT" in
    1.11 +  dvi | dvi.gz | ps | ps.gz | pdf)
    1.12 +    ;;
    1.13 +  *)
    1.14 +    fail "Bad output format '$OUTFORMAT'"
    1.15 +    ;;
    1.16 +esac
    1.17 +
    1.18 +
    1.19 +# prepare document
    1.20  
    1.21  cd "$DIR" || fail "Bad directory '$DIR'"
    1.22  
    1.23 +function pre_latex ()
    1.24 +{
    1.25 +  local FMT="$1"
    1.26 +  if [ -f root.bib ]
    1.27 +  then
    1.28 +    $ISATOOL latex -o "$FMT" && \
    1.29 +    $ISATOOL latex -o bbl && \
    1.30 +    $ISATOOL latex -o "$FMT"
    1.31 +  else
    1.32 +    $ISATOOL latex -o "$FMT"
    1.33 +  fi
    1.34 +}
    1.35 +
    1.36  if [ -f IsaMakefile ]; then
    1.37    $ISATOOL make "$OUTFORMAT"
    1.38    RC=$?   #FIXME !??
    1.39  elif [ "$OUTFORMAT" = pdf ]; then
    1.40 -  $ISATOOL latex -o pdf && $ISATOOL latex -o pdf
    1.41 +  pre_latex pdf && \
    1.42 +  $ISATOOL latex -o pdf
    1.43    RC=$?
    1.44  else
    1.45 -  $ISATOOL latex -o dvi && $ISATOOL latex -o "$OUTFORMAT"
    1.46 +  pre_latex dvi && \
    1.47 +  $ISATOOL latex -o "$OUTFORMAT"
    1.48    RC=$?
    1.49  fi
    1.50  
    1.51  
    1.52 -#install
    1.53 +# install
    1.54  
    1.55  [ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
    1.56  cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"