On Fri, 9 Dec 2022 14:35:44 GMT, Christoph Langer <clan...@openjdk.org> 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
