Re: Texinfo 7.0 changed the name of HTML output directory

[Patrice Dumas]

On Sun, Aug 25, 2024 at 11:33:45AM +0100, Gavin Smith wrote:
> 
> I think it is most likely a mistake.

Another possibility would be that the manual name got renamed and the
old name is used here.  But even if it was the case, the new name should
be there too, and there should be a comment explaining the situation.

-- 
Pat