On Fri, 13 Nov 2020 17:02:24 GMT, Daniel Fuchs <dfuchs at openjdk.org> wrote: >> Looks okay. > > @msheppar Good suggestions! I have updated the PR. The previous iteration was a cleaner but okay. ------------- PR: https://git.openjdk.java.net/jdk/pull/1144