On Wed, 14 Jul 2021 05:01:49 GMT, David Holmes <dholmes at openjdk.org> wrote: > Hi Thomas, > > This seems okay to me. > > Thanks, > David Thank you David and Volker! ------------- PR: https://git.openjdk.java.net/jdk/pull/4510