From a9c80b635526aa6007322c83df19f8f32c4d9dc1 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Wed, 26 May 2010 20:52:42 +0000
Subject: [PATCH] Adding contrib/my-configure

---
 contrib/my-configure | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100755 contrib/my-configure

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 $*
-- 
2.30.2