On Wed, 27 Nov 2024 10:13:13 GMT, Tobias Holenstein <tholenstein at openjdk.org> wrote: > Thanks for pointing those two things out. They should be fixed now! Thanks for fixing these! ------------- PR Comment: https://git.openjdk.org/jdk/pull/22402#issuecomment-2503565348