On Fri, 14 Feb 2025 10:17:53 GMT, Christian Hagedorn <chagedorn at openjdk.org> wrote: > Looks good and useful! Works as expected. Thanks, Christian! ------------- PR Comment: https://git.openjdk.org/jdk/pull/23621#issuecomment-2658917699