common/autoconf/generated-configure.sh
changeset 22478 5ca2b792a5fd
parent 22477 789f51111cb9
child 22709 540ed4c23085
--- a/common/autoconf/generated-configure.sh	Wed Jan 29 22:55:43 2014 +0100
+++ b/common/autoconf/generated-configure.sh	Fri Jan 31 10:24:58 2014 +0100
@@ -4087,7 +4087,7 @@
 #CUSTOM_AUTOCONF_INCLUDE
 
 # Do not change or remove the following line, it is needed for consistency checks:
-DATE_WHEN_GENERATED=1391032272
+DATE_WHEN_GENERATED=1391160222
 
 ###############################################################################
 #
@@ -48539,7 +48539,8 @@
   if test "x$CONFIGURE_OVERRIDDEN_VARIABLES" != x; then
     # Replace the separating ! with spaces before presenting for end user.
     unknown_variables=${CONFIGURE_OVERRIDDEN_VARIABLES//!/ }
-    as_fn_error $? "The following variables are unknown to configure: $unknown_variables" "$LINENO" 5
+    { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: The following variables might be unknown to configure: $unknown_variables" >&5
+$as_echo "$as_me: WARNING: The following variables might be unknown to configure: $unknown_variables" >&2;}
   fi