On 7/28/23 15:11, Joseph Myers wrote:
This patch is OK.
I fixed the whitespace errors in the patch as well as a couple minor ChangeLog entry items and pushed Costas's patch to the trunk.
jeff

Reply via email to