On Mon, 9 Oct 2023 05:39:19 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: > Looks good to me. Trivial, right? ------------- PR Comment: https://git.openjdk.org/jdk/pull/15533#issuecomment-1753182278