fix for source includes in gendoc.sh for future consideration

[Patrice Dumas]

Hello,

Here is a patch for gendocs.sh to be considered in the future.  It
allows to get the @include of the manual being targetted by gendocs.sh
and gather only the manual being targetted.

It uses a feature that was just added to the development version of
Texinfo, the addition of --trace-includes to texi2any/makeinfo to get
the list of a manual included files.  It also uses tar -T (--files-from)
to get the list of include files on stdin (as proposed by Bruno for a
past issue).

It seems to me that gendoc.sh is quite compatible with past versions of
Texinfo makeinfo.  Therefore I think that this patch is not acceptable
as is, there need to be a way to determine that the makeinfo version is
good, either by having an explicit command-line argument to turn on the
feature, or maybe checking $MAKEINFO --version, or something else.  I
think that if the makeinfo version does not have the future feature,
there should be fallback to the current situation with the *.texi*
globs.

I could propose an update version with the two possibilities, but I have
no idea on what would be an acceptable way to check whether makeinfo has
the right version.

Any remark on the approach?  Any idea on version checking or the like?

-- 
Pat

gendocs_trace_includes_files_from.diff
Description: Text Data