On Tue, 29 Mar 2022 at 23:40, Jacob Bachmeyer wrote: > > Rob Savoye wrote: > > On 3/29/22 04:13, Jonathan Wakely wrote: > >> 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 > >> > > > > I just updated the HTML manual pages on gnu.org, but still get a 404 > > on the config files. We'll have to look into that. I did add all the > > new pages though as the first step. > > > > - rob - > > They seem to all be there now; thanks for taking care of this, Rob.
Yes, it looks fine now, thanks!
