On Sun, Oct 23, 2022 at 08:36:04PM +0200, Bruno Haible wrote: > Therefore, on this platform, instead of picking the 'awk' that is found > in $PATH, it is a better strategy to look for 'nawk' or 'gawk' in $PATH.
Thanks for investigating this. I've made it try nawk as well: diff --git a/configure.ac b/configure.ac index 1cd323cff4..d0c2f9f530 100644 --- a/configure.ac +++ b/configure.ac @@ -77,7 +77,7 @@ AC_REQUIRE_AUX_FILE([tap-driver.sh]) # awk for texindex. # don't use AC_PROG_AWK because this prefers gawk, which is much slower # than mawk for texindex and texi2dvi -AC_CHECK_PROGS([TI_AWK], [awk mawk gawk], []) +AC_CHECK_PROGS([TI_AWK], [nawk mawk awk gawk], []) if test -z "$TI_AWK"; then AC_MSG_ERROR([awk not found]) fi
