On Fri, 27 Oct 2023 09:09:05 GMT, Jorn Vernee <jvernee at openjdk.org> wrote: > Do you want me to create a separate PR to remove the comment? No not necessary. Thanks ------------- PR Comment: https://git.openjdk.org/jdk/pull/16349#issuecomment-1784664238