On Wed, 23 Mar 2022 15:35:44 GMT, Erik Joelsson <er...@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. This pull request has now been integrated. Changeset: 1c4f5fcb Author: Erik Joelsson <er...@openjdk.org> URL: https://git.openjdk.java.net/jdk/commit/1c4f5fcb88892e6c76074eac87b63d81d53647b2 Stats: 1 line in 1 file changed: 0 ins; 0 del; 1 mod 8283575: Check for GNU time fails for version >1.7 Reviewed-by: shade, ihse ------------- PR: https://git.openjdk.java.net/jdk/pull/7925