[PATCH] docs/install.texi: Add note about not relying on gawk extensions

[David Malcolm]

OK for trunk?  ("make info" and "make dvi" seem to work, though I don't
have a dvi viewer handy).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: do-not-rely-on-gawk-extensions.patch
Type: text/x-patch
Size: 808 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20130725/d164fa42/attachment.bin>