diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 20:52:42 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-26 20:52:42 +0000 |
| commit | a9c80b635526aa6007322c83df19f8f32c4d9dc1 (patch) | |
| tree | 84caa5f00454173acdd95033f081078ca5c07784 /contrib/my-configure | |
| parent | 2f70d96546d82e6beb1e4492bfee46c962d9cfe4 (diff) | |
Adding contrib/my-configure
Diffstat (limited to 'contrib/my-configure')
| -rwxr-xr-x | contrib/my-configure | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/contrib/my-configure b/contrib/my-configure new file mode 100755 index 000000000..af5cb01f7 --- /dev/null +++ b/contrib/my-configure @@ -0,0 +1,9 @@ +#! /bin/bash + +CONFIG_OPTIONS= + +if [ -e .cvc4_config ]; then + CONFIG_OPTIONS=`cat .cvc4_config` +fi + +echo ./configure $CONFIG_OPTIONS $* |