No need to run make twice here.

a3cdea81 · Fred Drake · 304b91ea · a3cdea81
Commit a3cdea81 authored Oct 25, 2001 by Fred Drake
Hide whitespace changes
Inline Side-by-side

Showing with 0 additions and 1 deletion

Doc/tools/push-docs.sh Doc/tools/push-docs.sh +0 -1

No files found.
--- 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"