diff --git a/bin/BuildPackages.sh b/bin/BuildPackages.sh index 6c60cecee6..d0121c2f66 100755 --- a/bin/BuildPackages.sh +++ b/bin/BuildPackages.sh @@ -168,8 +168,11 @@ run_configure_and_make() { if grep Autoconf ./configure > /dev/null then echo_run ./configure --with-gaproot="$GAPROOT" $CONFIGFLAGS + echo_run "$MAKE" clean else echo_run ./configure "$GAPROOT" + echo_run "$MAKE" clean + echo_run ./configure "$GAPROOT" fi echo_run "$MAKE" else