On Tue, 6 Jun 2023 08:51:33 GMT, Daniel Fuchs <dfuchs at openjdk.org> wrote: > FWIW the changes look good to me. Thanks for looking into it. ------------- PR Comment: https://git.openjdk.org/jdk/pull/14280#issuecomment-1578414732