diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-07-03 18:18:55 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-07-03 18:18:55 +0000 |
| commit | 08c7de43f3ea028a9d397b09504d805affa39eef (patch) | |
| tree | e5648db382b10ec647479ba672574a243e768e2d /configure.ac | |
| parent | 6759aa95d4057a2a058974991bf7c9858899a477 (diff) | |
better config.reconfig script auto-generated
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 |