On Tue, 21 Feb 2023 21:27:08 GMT, Eirik Bjorsnos <duke at openjdk.org> wrote: > The last commit to #12623 introduced a compilation error caused by an extra semicolon. This PR fixes this. Marked as reviewed by naoto (Reviewer). ------------- PR: https://git.openjdk.org/jdk/pull/12701