On Tue, 30 May 2023 13:40:42 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: > Looks good and trivial. Thanks @TobiHartmann . ------------- PR Comment: https://git.openjdk.org/jdk/pull/14218#issuecomment-1568458529