tuned -c option;
authorwenzelm
Sat Apr 01 20:16:56 2000 +0200 (2000-04-01 ago)
changeset 865438ce936acb99
parent 8653 a88e91792f0a
child 8655 16906e600c9a
tuned -c option;
lib/Tools/document
     1.1 --- a/lib/Tools/document	Sat Apr 01 20:15:55 2000 +0200
     1.2 +++ b/lib/Tools/document	Sat Apr 01 20:16:56 2000 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    echo "Usage: $PRG [OPTIONS] [DIR]"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 -  echo "    -c           remove DIR after succesful run (!)"
     1.8 +  echo "    -c           cleanup -- be aggressive in removing old stuff"
     1.9    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    1.10    echo "                 ps.gz, pdf"
    1.11    echo
    1.12 @@ -81,7 +81,7 @@
    1.13  function pre_latex ()
    1.14  {
    1.15    local FMT="$1"
    1.16 -  rm -f *.aux *.out
    1.17 +  [ -n "$CLEAN" ] && rm -f *.aux *.out
    1.18    if [ -f root.bib ]
    1.19    then
    1.20      $ISATOOL latex -o "$FMT" && \
    1.21 @@ -95,6 +95,8 @@
    1.22  (
    1.23    cd "$DIR" || fail "Bad directory '$DIR'"
    1.24  
    1.25 +  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
    1.26 +
    1.27    if [ -f IsaMakefile ]; then
    1.28      $ISATOOL make "$OUTFORMAT"
    1.29      RC=$?