changeset 77:2e60b888e526

Try distclean before clean (otherwise we can end up trying to add to archives of the wrong arch for example)
author Chris Cannam
date Thu, 30 Oct 2014 16:06:26 +0000
parents a76b96026c2d
children ab0dbbb58119
files SCRIPTS/process.sh
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/SCRIPTS/process.sh	Thu Oct 30 13:25:15 2014 +0000
+++ b/SCRIPTS/process.sh	Thu Oct 30 16:06:26 2014 +0000
@@ -252,7 +252,9 @@
     if configure_maybe "$dir"; then
 	mfile=$(find_makefile "$dir")
 	if [ -n "$mfile" ]; then
-	    if make -C "$dir" -f "$mfile" clean; then
+	    if make -C "$dir" -f "$mfile" distclean; then
+		build "$dir"
+	    elif make -C "$dir" -f "$mfile" clean; then
 		build "$dir"
 	    else
 		echo "Failed to 'make clean' in $dir!" | tee "$log"