On Wed, Aug 16, 2023 at 4:32 PM Thomas Munro <thomas(dot)munro(at)gmail(dot)com> wrote:
> Does anyone else want to object? Restating the case in brief: commit
> 31966b15's naming is short-sighted and likely to lead to a
> proliferation of similar things or a renaming in later releases.
+1 to proceeding with this change.
--
Peter Geoghegan