On Fri, 16 Dec 2022 19:48:12 GMT, Nikita Gubarkov <[email protected]> wrote:
>> OK, I will submit a PR to take care of this soon. > > Thank you. Pushed under bug https://bugs.openjdk.org/browse/JDK-8298974 ------------- PR: https://git.openjdk.org/jdk/pull/4798
