diff options
Diffstat (limited to 'configure.ac')
| -rw-r--r-- | configure.ac | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/configure.ac b/configure.ac index ae681d2eb..f22ae595a 100644 --- a/configure.ac +++ b/configure.ac @@ -300,11 +300,11 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then cat >config.reconfig <<EOF [#!/bin/bash # Generated by configure, `date` -# This script part of CVC4. +# This script is part of CVC4. cd "\`dirname \\"\$0\\"\`" -current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\\+\\)/\\(.*\\),\\1 \\2,'\`) +current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`) arch=\${current[0]} build=\${current[1]} |