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 @@
 	    DISCARD_TEMPS=''
 	    shift 1
 	    ;;
+	-q|--quiet|__quie|--qui|--qu|--q)
+	    QUIET=true
+	    shift 1
+	    ;;
 	-*)
 	    usage
 	    ;;
@@ -119,6 +123,10 @@
     set -x
 fi
 
+if [ "$QUIET" ] ; then
+    exec >/dev/null
+fi
+
 for FILE in $@ ; do
     FILE=${FILE%.tex}
     if [ "$BUILD_DVI" -o "$BUILD_PS" ] ; then