diff options
| -rwxr-xr-x | Doc/tools/mkhowto.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Doc/tools/mkhowto.sh b/Doc/tools/mkhowto.sh index 6d8da8f..0541c85 100755 --- a/Doc/tools/mkhowto.sh +++ b/Doc/tools/mkhowto.sh @@ -99,6 +99,10 @@ while [ "$1" ] ; do DISCARD_TEMPS='' shift 1 ;; + -q|--quiet|__quie|--qui|--qu|--q) + QUIET=true + shift 1 + ;; -*) usage ;; @@ -119,6 +123,10 @@ if [ "$DEBUGGING" ] ; then set -x fi +if [ "$QUIET" ] ; then + exec >/dev/null +fi + for FILE in $@ ; do FILE=${FILE%.tex} if [ "$BUILD_DVI" -o "$BUILD_PS" ] ; then |