On Fri, 9 Dec 2022 14:35:44 GMT, Christoph Langer <[email protected]> wrote:
> Thanks, that's the kind of suggestions I was hoping for from the build > experts. 😄 I pushed a commit, let's see if it works... Hm, obviously not... I guess there must be some indentation error still... ------------- PR: https://git.openjdk.org/jdk20/pull/9
