From a281665972128869dce1aaa23850cd68a889171e Mon Sep 17 00:00:00 2001 From: Fred Drake Date: Thu, 25 Oct 2001 15:13:30 +0000 Subject: [PATCH] No need to run make twice here. --- Doc/tools/push-docs.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh index 381b160455..11a5f336ea 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" -- 2.40.0