On 8/27/20 5:05 PM, Jesper Wilhelmsson wrote: > Btw. I'd be happy to include some documentation around this in the OpenJDK Developers' Guide once it's settled how to do things. > /Jesper > Very helpful indeed, thanks.