1.1 --- a/common/autoconf/generated-configure.sh Fri Jun 28 12:00:03 2013 +0200
1.2 +++ b/common/autoconf/generated-configure.sh Fri Jun 28 12:02:37 2013 +0200
1.3 @@ -799,6 +799,7 @@
1.4 PKG_CONFIG
1.5 CODESIGN
1.6 XATTR
1.7 +IS_GNU_TIME
1.8 TIME
1.9 STAT
1.10 HG
1.11 @@ -3785,7 +3786,7 @@
1.12 #CUSTOM_AUTOCONF_INCLUDE
1.13
1.14 # Do not change or remove the following line, it is needed for consistency checks:
1.15 -DATE_WHEN_GENERATED=1372413413
1.16 +DATE_WHEN_GENERATED=1372413705
1.17
1.18 ###############################################################################
1.19 #
1.20 @@ -10472,6 +10473,14 @@
1.21 fi
1.22
1.23
1.24 +# Check if it's GNU time
1.25 +IS_GNU_TIME=`$TIME --version 2>&1 | $GREP 'GNU time'`
1.26 +if test "x$IS_GNU_TIME" != x; then
1.27 + IS_GNU_TIME=yes
1.28 +else
1.29 + IS_GNU_TIME=no
1.30 +fi
1.31 +
1.32
1.33 if test "x$OPENJDK_TARGET_OS" = "xwindows"; then
1.34
