option -c;
authorwenzelm
Wed Feb 09 12:28:44 2000 +0100 (2000-02-09)
changeset 8217dc3b8cdbb816
parent 8216 e4b3192dfefa
child 8218 6c4bec5cd2ac
option -c;
lib/Tools/document
     1.1 --- a/lib/Tools/document	Wed Feb 09 11:45:10 2000 +0100
     1.2 +++ b/lib/Tools/document	Wed Feb 09 12:28:44 2000 +0100
     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           clean -- remove DIR after succesful run"
     1.8 +  echo "    -c           remove DIR after succesful run (!)"
     1.9    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
    1.10    echo "                 ps.gz, pdf"
    1.11    echo
    1.12 @@ -115,7 +115,7 @@
    1.13    [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    1.14      cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
    1.15  
    1.16 -  exit $RC
    1.17 +  exit "$RC"
    1.18  )
    1.19  RC=$?
    1.20