On Mon, 20 Jan 2025 13:45:31 GMT, Robbin Ehn <rehn at openjdk.org> wrote: > Looks good. Thank you! ------------- PR Comment: https://git.openjdk.org/jdk/pull/23130#issuecomment-2604368604