On Thu, 6 Jan 2022 12:31:49 GMT, Christian Hagedorn <chagedorn at openjdk.org> wrote: > Two more things I've noticed: Thanks Christian. Does the last commit cover your comments? ------------- PR: https://git.openjdk.java.net/jdk/pull/6882