On Sun, 29 Dec 2024, 13:55 Gerald Pfeifer wrote: > I pushed the following for now, though
Thanks! something tells me this is not the > full extent of this issue. Something to dig into when I find more time. > What's your concern? I think the explanation for this is simple, and not likely to be part of a bigger issue. It should be easy to check, just delete all files under doc/html/manual and regenerate them. Any files which are not recreated are orphaned and should have been removed by previous commits (as this file should have been).
