diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 20:54:40 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 20:54:40 +0000 |
| commit | 4e62744f9c95906c69696ed0a0d46269ecb83381 (patch) | |
| tree | 4b0802ccdd261b7b5f63f2aae93d6c85a3955cfa /contrib | |
| parent | a9c80b635526aa6007322c83df19f8f32c4d9dc1 (diff) | |
Fixing my-configure
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/my-configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/my-configure b/contrib/my-configure index af5cb01f7..dce46fc67 100755 --- a/contrib/my-configure +++ b/contrib/my-configure @@ -6,4 +6,4 @@ if [ -e .cvc4_config ]; then CONFIG_OPTIONS=`cat .cvc4_config` fi -echo ./configure $CONFIG_OPTIONS $* +./configure $CONFIG_OPTIONS $* |