On Tue, 11 Apr 2023 13:02:29 GMT, Daniel Fuchs <dfuchs at openjdk.org> wrote: > Maybe wait until Daniel or Michael get a chance to look at the fix before integrating. Certainly. ------------- PR Comment: https://git.openjdk.org/jdk/pull/13424#issuecomment-1503327443