On 5/21/20, 9:52 PM, "Thomas Munro" <thomas(dot)munro(at)gmail(dot)com> wrote:> Here's a version with a commit message added. I'll push this to all> releases in a day or two if there are no objections.
Looks good to me. Thanks!
Nathan