A recently integrated PR (https://github.com/openjdk/jdk/pull/27398) ignored reviewer comments that arrived after the integration. The reviewer had requested better documentation. We will add this documentation in a separate PR.