On Wed, 10 May 2023 16:10:27 GMT, Christian Hagedorn <chagedorn at openjdk.org> wrote: > That looks reasonable. Thanks for reviewing this @chhagedorn ------------- PR Comment: https://git.openjdk.org/jdk/pull/13901#issuecomment-1543539946