On Thu, Aug 17 2023, Eli Zaretskii wrote:

> I intended to install this once there are no more review comments, as
> I think this could be a useful addition.  I believe Mattias also
> thought the idea was a good one.  So my preference is for you to post
> an updated patch, yes.

Here it is: