On Thu, 18 May 2023 21:45:43 GMT, Daniel D. Daugherty <dcu...@openjdk.org> 
wrote:

> Thumbs up. This fix is trivial.

Thanks, Dan!

-------------

PR Comment: https://git.openjdk.org/jdk/pull/14048#issuecomment-1553723344

Reply via email to