Adding documentation to my-configure

diff --git a/contrib/my-configure b/contrib/my-configure
index dce46fc6791cfdbc106d9ae5ebd52c7abffa7758..65a64895d6fccba8ff01df5792aee8469bdac8bb 100755 (executable)
--- a/contrib/my-configure
+++ b/contrib/my-configure
@@ -1,3 +1,6 @@
+# Includes the contents of the file .cvc4_config, if it exists, 
+# on the ./configure command line
+
 #! /bin/bash
 
 CONFIG_OPTIONS=