On Fri, 1 Dec 2023 08:45:00 GMT, Robbin Ehn <rehn at openjdk.org> wrote: > My time is a bit constrained right now, hopefully I can look at this next week. OK. There is no hurry. Take your time. ------------- PR Comment: https://git.openjdk.org/jdk/pull/16880#issuecomment-1835766167