[SCM] gawk branch, porting, updated. gawk-4.1.0-5157-g5ef9120f

[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  5ef9120f6f6c1292ddf7ce4a047b4945aa6a49dc (commit)
       via  b83112af7b45fc63b31239f40ca99c617c35c727 (commit)
       via  6477ed349723a4816ea6123dd8f8128d7a34431d (commit)
       via  381bf4c82c13e663172daa8d607ab91cd4bf919e (commit)
       via  66c36485ab9e5115789418a57d51cb301c5edd48 (commit)
      from  18a9e1bb28ccf172cd243cdc0f2164e9f818e209 (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=5ef9120f6f6c1292ddf7ce4a047b4945aa6a49dc

commit 5ef9120f6f6c1292ddf7ce4a047b4945aa6a49dc
Merge: 18a9e1bb b83112af
Author: Arnold D. Robbins <arnold@skeeve.com>
Date:   Fri Jul 8 10:11:58 2022 +0300

    Merge branch 'master' into porting


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

Summary of changes:
 doc/ChangeLog         |   4 +
 doc/gawkworkflow.info | 402 ++++++++++++++++++++++++++++++--------------------
 doc/gawkworkflow.texi | 334 ++++++++++++++++++++++++-----------------
 3 files changed, 437 insertions(+), 303 deletions(-)


hooks/post-receive
-- 
gawk