lib/Tools/document
changeset 9788 df671fa2562a
parent 8654 38ce936acb99
child 10511 efb3428c9879
     1.1 --- a/lib/Tools/document	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/document	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: prepare theory session document
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {
    1.18 @@ -58,9 +60,9 @@
    1.19  # args
    1.20  
    1.21  DIR="document"
    1.22 -[ $# -ge 1 ] && { DIR="$1"; shift; }
    1.23 +[ "$#" -ge 1 ] && { DIR="$1"; shift; }
    1.24  
    1.25 -[ $# -ne 0 ] && usage
    1.26 +[ "$#" -ne 0 ] && usage
    1.27  
    1.28  
    1.29  ## main
    1.30 @@ -84,11 +86,11 @@
    1.31    [ -n "$CLEAN" ] && rm -f *.aux *.out
    1.32    if [ -f root.bib ]
    1.33    then
    1.34 -    $ISATOOL latex -o "$FMT" && \
    1.35 -    $ISATOOL latex -o bbl && \
    1.36 -    $ISATOOL latex -o "$FMT"
    1.37 +    "$ISATOOL" latex -o "$FMT" && \
    1.38 +    "$ISATOOL" latex -o bbl && \
    1.39 +    "$ISATOOL" latex -o "$FMT"
    1.40    else
    1.41 -    $ISATOOL latex -o "$FMT"
    1.42 +    "$ISATOOL" latex -o "$FMT"
    1.43    fi
    1.44  }
    1.45  
    1.46 @@ -98,20 +100,20 @@
    1.47    [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
    1.48  
    1.49    if [ -f IsaMakefile ]; then
    1.50 -    $ISATOOL make "$OUTFORMAT"
    1.51 -    RC=$?
    1.52 +    "$ISATOOL" make "$OUTFORMAT"
    1.53 +    RC="$?"
    1.54    elif [ "$OUTFORMAT" = pdf ]; then
    1.55      pre_latex pdf && \
    1.56 -    $ISATOOL latex -o pdf && \
    1.57 +    "$ISATOOL" latex -o pdf && \
    1.58      { if [ -n "$ISABELLE_THUMBPDF" ]; then
    1.59 -        $ISATOOL latex -o png && \
    1.60 -        $ISATOOL latex -o pdf
    1.61 +        "$ISATOOL" latex -o png && \
    1.62 +        "$ISATOOL" latex -o pdf
    1.63        fi; }
    1.64 -    RC=$?
    1.65 +    RC="$?"
    1.66    else
    1.67      pre_latex dvi && \
    1.68 -    $ISATOOL latex -o "$OUTFORMAT"
    1.69 -    RC=$?
    1.70 +    "$ISATOOL" latex -o "$OUTFORMAT"
    1.71 +    RC="$?"
    1.72    fi
    1.73  
    1.74    [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    1.75 @@ -119,7 +121,7 @@
    1.76  
    1.77    exit "$RC"
    1.78  )
    1.79 -RC=$?
    1.80 +RC="$?"
    1.81  
    1.82  
    1.83  # install