--- 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