On Fri, 2 Jun 2023 05:03:20 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: > Looks good and trivial. Thanks for reviewing, Tobias! ------------- PR Comment: https://git.openjdk.org/jdk/pull/14272#issuecomment-1573225050