On 7/23/20 11:46 AM, Langer, Christoph wrote: > Bug: https://bugs.openjdk.java.net/browse/JDK-8237182 > Original Change: https://hg.openjdk.java.net/jdk/jdk/rev/14c78683c9f0 > Webrev: http://cr.openjdk.java.net/~clanger/webrevs/8237182.11u.0/ This looks fine, thank you. -- -Aleksey