On Sat, Feb 05, 2022 at 02:36:47PM +0100, Patrice Dumas wrote: > > > I believe it is the gendocs.sh script from Gnulib that is used by many > > GNU packages for building web documentation; we should check this > > still works with any changes.
I checked, and unless I missed something, --output is always used, and the manual is moved to a directory named especially, like texinfo/html_node/. So that should be ok. -- Pat
