On Mon, 22 May 2023 14:09:22 GMT, Martin Doerr <mdo...@openjdk.org> wrote:
>> Yes, good idea. > > Please take a look at > https://github.com/openjdk/jdk/pull/12708/commits/70736be631e4f1bf3fd3c0d45ddfc076b74ef9dd It looks good. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/12708#discussion_r1200576857
