On Mon, 20 Oct 2025 12:37:49 GMT, Tobias Hartmann <thartmann at openjdk.org> wrote: >> The extra letters removed. > > Looks good and trivial. Thanks @TobiHartmann ------------- PR Comment: https://git.openjdk.org/jdk/pull/27897#issuecomment-3422499813