diff options
Diffstat (limited to 'configure.ac')
-rw-r--r-- | configure.ac | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/configure.ac b/configure.ac index 0bced3680..49e35f71e 100644 --- a/configure.ac +++ b/configure.ac @@ -281,15 +281,20 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then cd ../../.. if test $exitval -eq 0; then cat >config.reconfig <<EOF -#!/bin/sh -ex +[#!/bin/bash # Generated by configure, `date` # This script part of CVC4. -target='$target' -build_type='$build_type' +cd "\`dirname \\"\$0\\"\`" -cd "builds/$target/$build_type" -./config.status "\$@" +current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\\+\\)/\\(.*\\),\\1 \\2,'\`) +arch=\${current[0]} +build=\${current[1]} + +echo "reconfiguring in builds/\$arch/\$build..." +cd "builds/\$arch/\$build" +echo ./config.status "\$@" +./config.status "\$@"] EOF chmod +x config.reconfig fi |