On 7/2/20 11:03 PM, rkennke at redhat.com wrote: > Bug: > https://bugs.openjdk.java.net/browse/JDK-8248725 > Webrev: > http://cr.openjdk.java.net/~rkennke/JDK-8248725/ Looks fine. > Is the right way to push this to: http://hg.openjdk.java.net/jdk/jdk15/ > ? Yes, I think so. -- Thanks, -Aleksey