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 trivial only after reviewing the issue and knowing the background. The PR description could be a bit more complete and save a bunch of clicking around. ------------- Marked as reviewed by rriggs (Reviewer). PR Review: https://git.openjdk.org/jdk/pull/15385#pullrequestreview-1589653044
