# HG changeset patch
# User Chris Cannam
# Date 1407412917 -3600
# Node ID 5638274646286987b3ee840a03ce2233365fa5f0
# Parent  b57cdd4f273eb93ae848f9a569fa531290cac13e
If building from clean, always re-run configure as well

diff -r b57cdd4f273e -r 563827464628 SCRIPTS/process.sh
--- a/SCRIPTS/process.sh	Thu Aug 07 12:13:21 2014 +0100
+++ b/SCRIPTS/process.sh	Thu Aug 07 13:01:57 2014 +0100
@@ -176,9 +176,13 @@
 
 configure_maybe() {
     dir="$1"
-    mfile=$(find_makefile "$dir")
-    if [ -z "$mfile" ]; then
-	configure "$dir"
+    if [ t"$do_rebuild" = t"yes" ]; then
+        configure "$dir"
+    else
+        mfile=$(find_makefile "$dir")
+        if [ -z "$mfile" ]; then
+	    configure "$dir"
+        fi
     fi
 }