From: Thomas Munro <thomas.munro@gmail.com> Sent: Monday, 4 November 2019 1:43 PM
> No comment on the patch but I noticed that the documentation changes don't build. Please make sure you can "make
docs"successfully, having installed the documentation tools[1].
Thanks for the feedback. An updated patch which fixes the docs issue is attached.
Kind Regards.
Peter Smith
---
Fujitsu Australia