On Wed, 10 Aug 2022 15:42:24 GMT, Thomas Stuefe <stuefe at openjdk.org> wrote: > This PR builds on #9801. Ah I see. I don't like it that much, but for now it's ok. ------------- PR: https://git.openjdk.org/jdk/pull/9802