On Tue, 9 Jul 2024 12:26:01 GMT, Thomas Stuefe <stuefe at openjdk.org> wrote: > Wait, didn't I fix this already? Weird, I could have sworn I fixed that. Ah well. ------------- PR Comment: https://git.openjdk.org/jdk/pull/20072#issuecomment-2217557748