On Mon, 24 Apr 2023 09:17:19 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: > Good job in nailing this down! The fix looks reasonable to me. Thanks, Tobias! ------------- PR Comment: https://git.openjdk.org/jdk/pull/13605#issuecomment-1519711177