projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: a9c80b6)
Fixing my-configure
authorChristopher L. Conway <christopherleeconway@gmail.com>
Wed, 26 May 2010 20:54:40 +0000 (20:54 +0000)
committerChristopher L. Conway <christopherleeconway@gmail.com>
Wed, 26 May 2010 20:54:40 +0000 (20:54 +0000)
contrib/my-configure patch | blob | history

diff --git a/contrib/my-configure b/contrib/my-configure
index af5cb01f7ccf5e127bf87b75edb6b6e6b1542014..dce46fc6791cfdbc106d9ae5ebd52c7abffa7758 100755 (executable)
--- 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 $*