On Tue, 9 May 2023 17:42:21 GMT, Sergey Bylokhov <s...@openjdk.org> wrote:
>> It should, and this is another point about not changing the documentation. > > Then let's not update it. Backed out doc changes. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/13830#discussion_r1188950338
