On Fri, 13 Oct 2023 15:02:10 GMT, Daniel Jeliński <djelin...@openjdk.org> wrote:
> …will file a follow-up PR once this one is merged You can submit it right away, so that we'll not forget about it. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/13261#discussion_r1358385429
