common/autoconf/generated-configure.sh
changeset 18425 768f15fff30a
parent 18423 5f706ddb73ed
child 18426 bf9e616c1476
--- a/common/autoconf/generated-configure.sh	Fri Jun 28 12:00:03 2013 +0200
+++ b/common/autoconf/generated-configure.sh	Fri Jun 28 12:02:37 2013 +0200
@@ -799,6 +799,7 @@
 PKG_CONFIG
 CODESIGN
 XATTR
+IS_GNU_TIME
 TIME
 STAT
 HG
@@ -3785,7 +3786,7 @@
 #CUSTOM_AUTOCONF_INCLUDE
 
 # Do not change or remove the following line, it is needed for consistency checks:
-DATE_WHEN_GENERATED=1372413413
+DATE_WHEN_GENERATED=1372413705
 
 ###############################################################################
 #
@@ -10472,6 +10473,14 @@
 fi
 
 
+# Check if it's GNU time
+IS_GNU_TIME=`$TIME --version 2>&1 | $GREP 'GNU time'`
+if test "x$IS_GNU_TIME" != x; then
+  IS_GNU_TIME=yes
+else
+  IS_GNU_TIME=no
+fi
+
 
 if test "x$OPENJDK_TARGET_OS" = "xwindows"; then