On Fri, 12 Aug 2022 06:17:12 GMT, Robbin Ehn <[email protected]> wrote:
>> David Holmes has updated the pull request incrementally with one additional >> commit since the last revision: >> >> Suggestion from Thomas > > Thanks! Thanks @robehn ! ------------- PR: https://git.openjdk.org/jdk/pull/9803
