Ticket #1110: configure.patch

configure

@@ -100 +100 @@
 exit 1
 fi
 
+if [ -e config.log ] ; then
+    PCONF=`cat config.log | tail -n 1 | grep configure`
+    if test x"$PCONF" != x"" ; then
+        PCONF=`echo $PCONF | sed 's/.\/configure//g'`
+    fi
+    for opt do
+        if test x"$opt" = x"--prev" -o x"$opt" = x"--previous" ; then
+            if test x"$PCONF" != "--prev" ; then
+                echo "Options: $PCONF"
+                ./configure $PCONF
+                exit
+            fi
+        fi
+    done
+fi
+
+CONFIGURATION_OPTS=""
 for opt do
+  CONFIGURATION_OPTS="$CONFIGURATION_OPTS ""$opt"
+done
+
+date >> config.log
+echo "   $0$CONFIGURATION_OPTS" >> config.log
+
+for opt do
   case "$opt" in
   --prefix=*) prefix=`echo $opt | cut -d '=' -f 2`
   ;;