Pushed: http://hg.openjdk.java.net/jdk/jdk/rev/801bd63c32f2 Thanks. On 2020/4/8, 11:11 PM, "Roland Westrelin" <rwestrel at redhat.com> wrote: > Do you think it's trivial to be pushed now? Yes I think it is. Roland.