On Wed, 28 Oct 2020 10:07:50 GMT, Andrew Dinn <adinn at openjdk.org> wrote: > This is arguably trivial and needs no review but here is one anyway. Thanks @adinn for your review. Pushed. ------------- PR: https://git.openjdk.java.net/jdk/pull/854