lib/Tools/document
changeset 11844 eb072fd9a45a
parent 11581 d7bb261e3a3b
child 11948 9c812b21b2e8
     1.1 --- a/lib/Tools/document	Sat Oct 20 20:14:56 2001 +0200
     1.2 +++ b/lib/Tools/document	Sat Oct 20 20:15:27 2001 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4    echo "    -c           cleanup -- be aggressive in removing old stuff"
     1.5    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
     1.6    echo "                 ps.gz, pdf"
     1.7 -  echo "    -v           be verbose"
     1.8    echo
     1.9    echo "  Prepare the theory session document in DIR (default 'document')"
    1.10    echo "  producing the specified output format."
    1.11 @@ -39,9 +38,8 @@
    1.12  
    1.13  CLEAN=""
    1.14  OUTFORMAT=dvi
    1.15 -VERBOSE=""
    1.16  
    1.17 -while getopts "co:v" OPT
    1.18 +while getopts "co:" OPT
    1.19  do
    1.20    case "$OPT" in
    1.21      c)
    1.22 @@ -50,9 +48,6 @@
    1.23      o)
    1.24        OUTFORMAT="$OPTARG"
    1.25        ;;
    1.26 -    v)
    1.27 -      VERBOSE=true
    1.28 -      ;;
    1.29      \?)
    1.30        usage
    1.31        ;;
    1.32 @@ -122,8 +117,7 @@
    1.33    fi
    1.34  
    1.35    if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
    1.36 -    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \
    1.37 -    [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2
    1.38 +    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
    1.39    fi
    1.40  
    1.41    exit "$RC"