On Mon, 11 Sep 2023 22:45:42 GMT, Vicente Romero <vromero at openjdk.org> wrote: > why keeping this if it won't be used? Sure; I can delete that before the changeset goes back. ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/14432#discussion_r1327811884