On Mon, 21 Nov 2022 08:10:28 GMT, Robbin Ehn <rehn at openjdk.org> wrote: > Looks good, thank you! Thanks! Do you want to record this as "formal" PR review, not just a comment? ------------- PR: https://git.openjdk.org/jdk/pull/11194