On 14/11/2025 11:32 am, Juergen Gross wrote: > Some paths in config/Paths.mk.in are used nowhere, so remove them. > > Signed-off-by: Juergen Gross <[email protected]> > --- > config/Paths.mk.in | 5 ----- > 1 file changed, 5 deletions(-) > > diff --git a/config/Paths.mk.in b/config/Paths.mk.in > index bc42748b7a..668545be2f 100644 > --- a/config/Paths.mk.in > +++ b/config/Paths.mk.in > @@ -20,10 +20,7 @@ libexecdir := @libexecdir@ > datarootdir := @datarootdir@ > mandir := @mandir@ > docdir := @docdir@ > -dvidir := @dvidir@ > htmldir := @htmldir@ > -pdfdir := @pdfdir@ > -psdir := @psdir@
The point I apparently didn't make very well was this: We generate both HTML and PDFs, yet use neither of htmldir nor pdfdir. Whatever is done to one should be done to the other. Leave just docdir, and let whomever tidies up the mess in docs/ adjust the paths as necessary. ~Andrew
