On Thu, 9 Feb 2023 07:16:48 GMT, David Holmes <dholmes at openjdk.org> wrote: > Seems fine and trivial (only 1 review needed). > > Thanks ------------- PR: https://git.openjdk.org/jdk/pull/12482