On 9/4/19 3:39 PM, Andrew John Hughes wrote: > > I looked this over when we were discussing it internally and it looks > fine to me. Please push. > Pushed: https://hg.openjdk.java.net/jdk7u/jdk7u/hotspot/rev/e00eb0a88cae Thanks, Martin.-