On Mon, 26 Feb 2024 01:17:23 GMT, Jaikiran Pai <jpai at openjdk.org> wrote: > Hello Christoph, yes that looks fine to me. I adjusted it to the given suggestion. ------------- PR Comment: https://git.openjdk.org/jdk/pull/17952#issuecomment-1967070481