[SCM] gawk branch, gawk-5.1-stable, updated. gawk-4.1.0-4149-gf7fc3e2

[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, gawk-5.1-stable has been updated
       via  f7fc3e29590612f4c67e39a2772e8ea2e3412f01 (commit)
      from  a3e187cbb5c9ef951152f18fee1d36c93e4abbe5 (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=f7fc3e29590612f4c67e39a2772e8ea2e3412f01

commit f7fc3e29590612f4c67e39a2772e8ea2e3412f01
Author: Arnold D. Robbins <arnold@skeeve.com>
Date:   Mon Oct 12 10:25:59 2020 +0300

    Small fix in gawkapi.c.

diff --git a/ChangeLog b/ChangeLog
index f5bc082..45025d4 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2020-10-12         Arnold D. Robbins     <arnold@skeeve.com>
+
+       * gawkapi.c (api_lintwarn): Fix comparison, should be to check
+       lintfunc, not lintwarn. Thanks to OLLIER Jean-François
+       <lalanne.51@wanadoo.fr>, reported 23 March, 2014.
+
 2020-10-11         Arnold D. Robbins     <arnold@skeeve.com>
 
        * re.c (make_regexp): Add {} to characters that cause rp->maybe_long
diff --git a/gawkapi.c b/gawkapi.c
index 3ae837f..c85427b 100644
--- a/gawkapi.c
+++ b/gawkapi.c
@@ -275,7 +275,7 @@ api_lintwarn(awk_ext_id_t id, const char *format, ...)
        (void) id;
 
        va_start(args, format);
-       if (lintwarn == r_fatal) {
+       if (lintfunc == r_fatal) {
                err(true, _("fatal: "), format, args);
        } else {
                err(false, _("warning: "), format, args);

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

Summary of changes:
 ChangeLog | 6 ++++++
 gawkapi.c | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)


hooks/post-receive
-- 
gawk