diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-19 23:36:21 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-19 23:36:21 +0000 |
| commit | 4d99bd48c1ec94aafd99aaefb74e9c526eecd499 (patch) | |
| tree | 3d913dd6e061b1f6d21be5ff7235e3047ed00399 /configure.ac | |
| parent | 255d7e4140d5fee6edfe5c7233c8870f889b2a32 (diff) | |
fix configure step on Ubuntu oneiric (11.10)-- related to bug #284
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 930a5685c..9d28d21fa 100644 --- a/configure.ac +++ b/configure.ac @@ -325,8 +325,8 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then $as_echo "cd builds/$target/$build_type" cd "builds/$target/$build_type" CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS - echo "../../../configure ${config_cmdline[[@]]}" - `pwd`/../../../configure "${config_cmdline[[@]]}" + echo "$SHELL ../../../configure ${config_cmdline[[@]]}" + "$SHELL" "`pwd`/../../../configure" "${config_cmdline[[@]]}" exitval=$? cd ../../.. if test $exitval -eq 0; then |