lib/Tools/document
changeset 11581 d7bb261e3a3b
parent 10555 2323ec838401
child 11844 eb072fd9a45a
     1.1 --- a/lib/Tools/document	Thu Sep 27 12:24:19 2001 +0200
     1.2 +++ b/lib/Tools/document	Thu Sep 27 12:24:40 2001 +0200
     1.3 @@ -18,6 +18,7 @@
     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 @@ -38,8 +39,9 @@
    1.12  
    1.13  CLEAN=""
    1.14  OUTFORMAT=dvi
    1.15 +VERBOSE=""
    1.16  
    1.17 -while getopts "co:" OPT
    1.18 +while getopts "co:v" OPT
    1.19  do
    1.20    case "$OPT" in
    1.21      c)
    1.22 @@ -48,6 +50,9 @@
    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 @@ -116,8 +121,10 @@
    1.33      RC="$?"
    1.34    fi
    1.35  
    1.36 -  [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
    1.37 -    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
    1.38 +  if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
    1.39 +    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \
    1.40 +    [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2
    1.41 +  fi
    1.42  
    1.43    exit "$RC"
    1.44  )