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. Looks okay, provided you tested with some version of GNU [Tt]ime. Is double square bracket some sort of escaping? Haven't seen it before. ------------- Marked as reviewed by shade (Reviewer). PR: https://git.openjdk.java.net/jdk/pull/7925
