It works for me also. Thanks.

On Thu, Jun 4, 2020 at 9:26 AM Dmitry Gutov <dgutov@yandex.ru> wrote:
On 04.06.2020 19:23, Alan Mackenzie wrote:
> Would you please try out the following patch, which ought to fix the
> problem the patch should fix.

I tried it a few days ago, and it indeed seemed to fix the reported
scenario.