> On 2 Jul 2020, at 15:32, Daniel Fuchs <daniel.fuchs at oracle.com> wrote: > > ... > > Webrev updated: > http://cr.openjdk.java.net/~dfuchs/webrev_8248703/webrev.01/ > > Is this still appropriate to push to 15 or should I rather aim at 16? LGTM. I don’t have a strong opinion which release this goes into. -Chris.