diff options
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/configure.ac b/configure.ac index de6b3a427..1635f938a 100644 --- a/configure.ac +++ b/configure.ac @@ -305,6 +305,8 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then cd "\`dirname \\"\$0\\"\`" +if test -d builds; then :; else echo 'No builds/ directory!' >&2; exit; fi + current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`) arch=\${current[0]} build=\${current[1]} |