diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh
index 381b160455d..11a5f336ea3 100755
--- a/Doc/tools/push-docs.sh
+++ b/Doc/tools/push-docs.sh
@@ -64,7 +64,6 @@ MYDIR="`pwd`"
 cd ..
 
 # now in .../Doc/
-make --no-print-directory || exit $?
 make --no-print-directory bziphtml || exit $?
 RELEASE=`grep '^RELEASE=' Makefile | sed 's|RELEASE=||'`
 PACKAGE="html-$RELEASE.tar.bz2"