RFR: 8283575: Check for GNU time fails for version >1.7 [v2]

Thu Mar 24 09:49:46 UTC 2022

On Wed, 23 Mar 2022 22:06:49 GMT, Erik Joelsson <erikj at openjdk.org> wrote:

>> The version output of GNU time changed from "GNU time" to "GNU Time" in version 1.8. We need to update our check for identifying GNU time to handle this.
>
> Erik Joelsson has updated the pull request incrementally with one additional commit since the last revision:
> 
>   Update make/autoconf/basic_tools.m4
>   
>   Co-authored-by: Magnus Ihse Bursie <mag at icus.se>

Marked as reviewed by ihse (Reviewer).

-------------

PR: https://git.openjdk.java.net/jdk/pull/7925