On Fri, 21 Nov 2025 15:59:36 GMT, Daniel Fuchs <dfuchs at openjdk.org> wrote: >> Comment added. > > Not seeing the comment - maybe you haven't pushed it? yeah, that was it. Pushed now - thanks for checking! ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/28195#discussion_r2550965329