On Tue, 24 May 2022 06:59:23 GMT, David Holmes <dholmes at openjdk.org> wrote: >> Thank you, fixed. > > I don't see it fixed :) My bad, the changes are pushed now :). ------------- PR: https://git.openjdk.java.net/jdk/pull/8748