Re: FYI: revamp Headers node

[Akim Demaille]

>>> "adl" == Alexandre Duret-Lutz <address@hidden> writes:

 > +For header files that are built and must not be distributed, use the
 > address@hidden prefix as in @code{nodist_include_HEADERS} or
 > address@hidden  If these generated headers are needed
 > +during the build, you must also ensure they exist before they are
 > +used, see @xref{Sources}.
 
Wow!  I had never realized there was this feature!  Then, maybe the
documentation lacks clarification of BUILT_SOURCES
vs. nodist_.*_SOURCES.  I have found no node covering the two
simultaneously, and at first sight, it looks to me like some uses of
BUILT_SOURCES in the documentation ought to refer to
nodist_.*_SOURCES.