[SCM] gawk branch, porting, updated. gawk-4.1.0-4280-gc722d6f

[Arnold Robbins]

This is an automated email from the git hooks/post-receive script. It was
generated because a ref change was pushed to the repository containing
the project "gawk".

The branch, porting has been updated
       via  c722d6fbf49796a50b628fd1728f69b505155a9f (commit)
       via  696533f3f4a3b2dd36042eac5e1dce6f9bcec129 (commit)
      from  934ce1af71c698534a74f0698fee9743264cf8ea (commit)

Those revisions listed above that are new to this repository have
not appeared on any other notification email; so we list those
revisions in full, below.

- Log -----------------------------------------------------------------
http://git.sv.gnu.org/cgit/gawk.git/commit/?id=c722d6fbf49796a50b628fd1728f69b505155a9f

commit c722d6fbf49796a50b628fd1728f69b505155a9f
Merge: 934ce1a 696533f
Author: Arnold D. Robbins <arnold@skeeve.com>
Date:   Sun Sep 13 21:03:03 2020 +0300

    Merge branch 'master' into porting


-----------------------------------------------------------------------

Summary of changes:
 awklib/eg/prog/egrep.awk |  67 +++--
 doc/ChangeLog            |   5 +
 doc/gawk.info            | 750 ++++++++++++++++++++++++-----------------------
 doc/gawk.texi            | 190 +++++++-----
 doc/gawktexi.in          | 190 +++++++-----
 5 files changed, 660 insertions(+), 542 deletions(-)


hooks/post-receive
-- 
gawk