No need to run make twice here.

diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh
index 381b160455ddeb0f36c3d88e60934c73bc0c7657..11a5f336ea3b0fb60330700c874804b2e5dfbf2d 100755 (executable)
--- 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"