On Fri, 9 Feb 2024 23:16:20 GMT, Christoph Langer <clan...@openjdk.org> wrote:
> I will integrate this in the next days unless somebody explicitly vetoes > (given that the PR shows reviews from 3 persons) I guess that would be OK, but we may revisit this to do one of the things I outlined above. ------------- PR Comment: https://git.openjdk.org/jdk/pull/17404#issuecomment-1937847536
