On Fri, 25 Aug 2023 14:56:45 GMT, Christian Hagedorn <chagedorn at openjdk.org> wrote: > Looks good and trivial! Thanks, Christian! ------------- PR Comment: https://git.openjdk.org/jdk/pull/15430#issuecomment-1693531477