On Mon, Apr 29, 2024 at 01:11:11AM +0200, Lorenzo Puliti wrote: > I think this change is worth a NEWS entry, with an example > that explains how to revert to the previous default. Sounds a good idea. Thanks. I'll queue your suggestion for the next upload. Best wishes, Mark