On Thu, 2020-01-16 at 23:43 +0000, Joseph Myers wrote:
> Thanks, patch committed.
Beat me to it :-)  I spun it yesterday, but didn't get around to
committing it.
jeff

Reply via email to