changeset 43:563827464628

If building from clean, always re-run configure as well
author Chris Cannam
date Thu, 07 Aug 2014 13:01:57 +0100
parents b57cdd4f273e
children 0036098a5edb
files SCRIPTS/process.sh
diffstat 1 files changed, 7 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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
 }