On Mon, 10 Jun 2024 08:57:23 GMT, Maurizio Cimadamore <mcimadamore at openjdk.org> wrote: > Good catch! Thanks! ------------- PR Comment: https://git.openjdk.org/jdk/pull/19620#issuecomment-2157910277