- Rename CONTRIBUTORS into CREDITS

- comply more accurately with the advertising clause of the Berkeley
and Gnuplot licenses

- update the texinfo tools to use @verbatiminclude instead of @include
(the included files don't need to be modified anymore--i.e., they can
be read directly by getdp/gmsh)

- generate full html and text versions of the documentation