On Wed, 5 Feb 2025 18:42:10 GMT, Daniel Fuchs <dfuchs at openjdk.org> wrote: > And implementing the suggested changes would be good... done, thanks ------------- PR Comment: https://git.openjdk.org/jdk/pull/23469#issuecomment-2637743071