On Fri, 7 Jun 2024 06:39:52 GMT, Robbin Ehn <rehn at openjdk.org> wrote: > Hope you are fine with this. OK. ------------- PR Comment: https://git.openjdk.org/jdk/pull/19556#issuecomment-2155874697