lib/Tools/latex
changeset 9788 df671fa2562a
parent 8568 b18540435f26
child 10511 efb3428c9879
     1.1 --- a/lib/Tools/latex	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/latex	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,11 +1,13 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: run LaTeX (and related tools)
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {
    1.18 @@ -53,9 +55,9 @@
    1.19  # args
    1.20  
    1.21  FILE="root.tex"
    1.22 -[ $# -ge 1 ] && { FILE="$1"; shift; }
    1.23 +[ "$#" -ge 1 ] && { FILE="$1"; shift; }
    1.24  
    1.25 -[ $# -ne 0 ] && usage
    1.26 +[ "$#" -ne 0 ] && usage
    1.27  
    1.28  
    1.29  ## main
    1.30 @@ -63,11 +65,8 @@
    1.31  # root file
    1.32  
    1.33  DIR=$(dirname "$FILE")
    1.34 -if [ "$DIR" = . ]; then
    1.35 -  FILEBASE=$(basename "$FILE" .tex)
    1.36 -else
    1.37 -  FILEBASE=$DIR/$(basename "$FILE" .tex)
    1.38 -fi
    1.39 +FILEBASE=$(basename "$FILE" .tex)
    1.40 +[ "$DIR" = . ] || FILEBASE="$DIR/$FILEBASE"
    1.41  
    1.42  function check_root () { [ -f "$FILEBASE.tex" ] || fail "Bad file '$FILE'"; }
    1.43  
    1.44 @@ -82,7 +81,7 @@
    1.45  
    1.46  function update_styles ()
    1.47  {
    1.48 -  for NAME in $ISABELLE_HOME/lib/texinputs/*.sty
    1.49 +  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
    1.50    do
    1.51      DEST="$DIR"/$(basename "$NAME")
    1.52      if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
    1.53 @@ -96,49 +95,49 @@
    1.54    dvi)
    1.55      check_root && \
    1.56      run_latex
    1.57 -    RC=$?
    1.58 +    RC="$?"
    1.59      ;;
    1.60    dvi.gz)
    1.61      check_root && \
    1.62      run_latex && \
    1.63      gzip -f "$FILEBASE.dvi"
    1.64 -    RC=$?
    1.65 +    RC="$?"
    1.66      ;;
    1.67    ps)
    1.68      check_root && \
    1.69      run_latex && \
    1.70      run_dvips &&
    1.71 -    RC=$?
    1.72 +    RC="$?"
    1.73      ;;
    1.74    ps.gz)
    1.75      check_root && \
    1.76      run_latex && \
    1.77      run_dvips &&
    1.78      gzip -f "$FILEBASE.ps"
    1.79 -    RC=$?
    1.80 +    RC="$?"
    1.81      ;;
    1.82    pdf)
    1.83      check_root && \
    1.84      run_pdflatex
    1.85 -    RC=$?
    1.86 +    RC="$?"
    1.87      ;;
    1.88    bbl)
    1.89      check_root && \
    1.90      run_bibtex
    1.91 -    RC=$?
    1.92 +    RC="$?"
    1.93      ;;
    1.94    png)
    1.95      check_root && \
    1.96      run_thumbpdf
    1.97 -    RC=$?
    1.98 +    RC="$?"
    1.99      ;;
   1.100    sty)
   1.101      update_styles
   1.102 -    RC=$?
   1.103 +    RC="$?"
   1.104      ;;
   1.105    *)
   1.106      fail "Bad output format '$OUTFORMAT'"
   1.107      ;;
   1.108  esac
   1.109  
   1.110 -exit $RC
   1.111 +exit "$RC"