On Fri, 2 Feb 2024 at 11:10, <rep.dot....@gmail.com> wrote: > > On 1 February 2024 18:15:34 CET, Christophe Lyon <christophe.l...@linaro.org> > wrote: > >BUILD_INFO is currently a byproduct of checking makeinfo > >presence/version. INSTALL_INFO used to be defined similarly, but was > >removed in 2000 (!) by commit 17db658241d18cf6db59d31bc2d6eac96e9257df > >(svn r38141). > > > >In order to save build time, our CI overrides BUILD_INFO="", which > >works when invoking 'make all' but not for 'make install' in case some > >info files need an update. > > Instead of resurrecting INSTALL_INFO maybe you could something along the > lines of > > https://gcc.gnu.org/bugzilla/attachment.cgi?id=15038&action=edit
Ha indeed something along these lines would work too. Thanks for the archaeology :-) > > not sure which approach would be considered cleaner.. Not sure either. What do maintainers prefer? > > HTH
