Hi Martin, I pushed to jdk repo, but have no clue on the process to get it to jdk11. -Zhengyu On 07/02/2018 03:35 PM, Martin Buchholz wrote: > > Can we have this fix make it into jdk11?