On Tue, 22 Aug 2023 14:55:18 GMT, Pavel Rappo <pra...@openjdk.org> wrote:
>> Please review this trivial PR. > > Pavel Rappo has updated the pull request with a new target base due to a > merge or a rebase. The pull request now contains two commits: > > - Merge branch 'master' into 8314753 > - Initial commit Looks good, thanks. ------------- Marked as reviewed by kevinw (Committer). PR Review: https://git.openjdk.org/jdk/pull/15385#pullrequestreview-1599820441