On Wed, 23 Mar 2022 22:06:49 GMT, Erik Joelsson 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
> 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
On Wed, 23 Mar 2022 15:35:44 GMT, Erik Joelsson 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.
I usually handle cases like this by prefixing with a comment:
#
On Wed, 23 Mar 2022 16:22:55 GMT, Aleksey Shipilev wrote:
> Looks okay, provided you tested with some version of GNU [Tt]ime.
Thanks! I hit this while trying to use GNU time on my mac to get LOG=profile to
work, to profile compilation times of individual compilation units. I built
latest
On Wed, 23 Mar 2022 15:35:44 GMT, Erik Joelsson 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
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.
-
Commit messages:
- JDK-8283575
Changes: https://git.openjdk.java.net/jdk/pull/7925/files
Webrev:
