Re: Build failure from git HEAD

[Pavel Raiskup]

On Tuesday, June 14, 2022 1:51:18 AM CEST Paul Eggert wrote:
> Thanks for reporting that. I installed the attached to fix it.

Indeed helped.  Thank you, Paul.
Pavel