On Fri, 7 Jul 2023 12:01:28 GMT, Daohan Qu <dqu at openjdk.org> wrote: > Okay! Thanks for your explanations, Thomas. I'll pay attention to that. No problem, and thanks for the fix. ------------- PR Comment: https://git.openjdk.org/jdk/pull/14782#issuecomment-1625367725