On Wed, 15 Nov 2023 08:18:39 GMT, Christian Hagedorn <chagedorn at openjdk.org> wrote: > Looks good to me, too! Thanks for reviewing and the suggestions. Comments applied in new commit. ------------- PR Comment: https://git.openjdk.org/jdk/pull/16581#issuecomment-1812878709