Am 30.01.2020 um 04:40 schrieb Sergey Bylokhov:
Thank you for this bug report, can you please file it: https://bugs.java.com/bugdatabase
I seem to have missed the link to that site from the OpenJDK-site for some reason but I remember the link from the Good Old Days[TM] ;-) Filed a bug report, thanks for pointing me to the form. Should be an easy fix in my eyes. Thanks and cheers, Lothar