On Mon, 14 Dec 2020 04:52:02 GMT, David Holmes <dholmes at openjdk.org> wrote: > Hi Thomas, > Not an expert but this all seems quite reasonable to me. > Thanks, > David Thanks David! ------------- PR: https://git.openjdk.java.net/jdk/pull/1757