# HG changeset patch
# User Chris Cannam
# Date 1414685186 0
# Node ID 2e60b888e526e6e8822e9d3cbb8cdb8b9dda23bc
# Parent  a76b96026c2d565a3493322aa2e0a722f98299f8
Try distclean before clean (otherwise we can end up trying to add to archives of the wrong arch for example)

diff -r a76b96026c2d -r 2e60b888e526 SCRIPTS/process.sh
--- 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"