Broken links in online HTML manual

Jonathan Wakely <[email protected]> Tue, 29 Mar 2022 11:13:18 +0100
Newsgroups gmane.comp.sysutils.dejagnu.general
Message-ID <CACb0b4=F=TrtfHd4CBKWwHHZR6f1=GPFC=z6X6KgOOOjmWfrhA@mail.gmail.com>
All the links for configuration files at
https://www.gnu.org/software/dejagnu/manual/index.html give a 404
error:
https://www.gnu.org/software/dejagnu/manual/Local-configuration-file.html
https://www.gnu.org/software/dejagnu/manual/Global-configuration-file.html
https://www.gnu.org/software/dejagnu/manual/Board-configuration-file.html
https://www.gnu.org/software/dejagnu/manual/Configuration-file-values.html

Several other pages of the manual are missing too:
https://www.gnu.org/software/dejagnu/manual/Running-other-DejaGnu-commands.html

This might be something to do with texinfo munging special characters
in node names.