On Wed, 14 Jun 2023 14:19:12 GMT, Robbin Ehn <rehn at openjdk.org> wrote: > Pushed an update after review comments, hope I got all! Still good. Thanks for taking my suggestions. ------------- PR Comment: https://git.openjdk.org/jdk/pull/14445#issuecomment-1591327943