[latexrefman-discuss] permission to incorporate latex docs into devdocs.io

[Karl Berry]

Hi Alex - the latex2e.texi license just says to preserve the license
notice, and hence allow users to further copy/modify.  It's the old GNU
documentation license (pre-GFDL).  So I don't see a problem with devdocs
providing a munged version.  Of course it would be nice to provide the
sources you use as well.

Also, we continue to actively work on latex2e.texi.  Given the plethora
of things I see on devdocs.io, I suppose you (they) have a process to
pull updates.  I hope so, since distributing stale information wouldn't
be especially helpful to anyone :).

Best,
Karl