license of generated info docs (GFDL?) and man pages

[Matthias Klose <doko at cs dot tu-berlin dot de>]

Looking at the source of the gcc docs, the GFDL-1.2 is mentioned. In
the generated html docs and in the generated man pages you can re-find
the copyright, but it's absent of the generated info docs. Some
questions:

- Are the generated info docs are covered by the GFDL, and
  especially are there any invariant sections?

- Assuming the description of the options will be generated from a
  common description in the sources (in 3.4 or later), will the output
  of gcc --help be put under the GFDL as well?

- Could the GCC project consider to re-license the man pages under a
  license, which would Debian allow to distribute these as part of the
  gcc package(s)?

Thanks, Matthias

Background: Debian doesn't see the GFDL (and especially the Invariant
sections) as a free license. As a consequence, the docs and man pages
have to be removed from the Debian packages. However it seems to be ok
to put these in a separate package in the "non-free" section, which is
built from another source package.

See http://bugs.debian.org/193787 for more information.