On Tue, 11 Oct 2022 15:48:56 GMT, Raffaello Giulietti <rgiulietti at openjdk.org> wrote: > Simple doc correction. Marked as reviewed by bpb (Reviewer). ------------- PR: https://git.openjdk.org/jdk/pull/10658