On 21/12/2023 18:46, Dmitry Gutov wrote:
> See instead the patch attached to this bug report.

Here's an update, incorporating the feedback from here and there.