On Wed, 11 Jun 2025, Peter Oliver wrote:

> Attached is a patch that does this, addressing both bugs 78747 and 78748.

Oops, forgot part of the fix for 78747.  Here¢s an improved patch.

-- 
Peter Oliver