On Tue, 27 Oct 2020 07:20:09 GMT, Robbin Ehn <rehn at openjdk.org> wrote: >> Okay, new version then, please take a look! > > Still fine! Cheers @robehn and @kimbarrett. Testing is still clean, so I am pushing. ------------- PR: https://git.openjdk.java.net/jdk/pull/863