diff options
Diffstat (limited to 'contrib/my-configure')
| -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 $* |