On Mon, 23 May 2022 09:22:52 GMT, Martin Doerr <mdoerr at openjdk.org> wrote: >> Yeah, that seems better to me as well. > > +1 Thanks for the feedback. I have made this change. ------------- PR: https://git.openjdk.java.net/jdk/pull/8754