Documentation: Linux kernel and GNU/Linux system

[Christophe Jarry]

Dear developers,

I am reading the documentation for gawk
(http://www.gnu.org/software/gawk/manual/gawk.html) and have found that
sometimes you use the term "Linux" instead of "GNU/Linux" to refer to
the system.

Here are the culprits:

* in "Foreword" section:
  "gawk ships with Linux, and you can download binaries or source code
  for almost any system; my wife uses gawk on her VMS box."

* in "The GNU Project and This Book":
  "Many GNU/Linux distributions are often available in computer stores
  or bundled on CD-ROMs with books about Linux."

* in "Glossary":
  "Linux is a stable, efficient, full-featured clone of Unix that has
  been ported to a variety of architectures."

* in "Index", "Linux:" references should be deleted ("GNU/Linux:"
references are already there and refer to the same sections), as there
is no reference to the Linux kernel in the related sections.

Please make the changes.

Thanks.

Christophe