There's no longer any reason to require GNU awk:

- the only part that required it (socks proxy settings) is gone,
- all remaining awk scripts are POSIXly correct (or should be).

 -------- diffstat follows --------
 /trunk/configure                     |    5     2     3     0 ++---
 /trunk/Makefile.in                   |    2     0     2     0 --
 /trunk/scripts/build/kernel/linux.sh |    2     1     1     0 +-
 /trunk/scripts/build/internals.sh    |    1     0     1     0 -
 /trunk/scripts/build/mpfr.sh         |    2     1     1     0 +-
 /trunk/scripts/functions             |    4     2     2     0 ++--
 /trunk/scripts/saveSample.sh.in      |    4     2     2     0 ++--
 7 files changed, 8 insertions(+), 12 deletions(-)

1 files changed, 2 insertions, 3 deletions

diff --git a/configure b/configure
index 39d0e7d0..cb22ca0a 100755
--- a/configure
+++ b/configure
@@ -4,9 +4,8 @@ VERSION=$( cat .version )
 DATE=$( date +%Y%m%d )
 
 # All absolutely required tools, one per line to ease diff.
-# See function 'has_or_abort, below, for syntax
+# See function 'has_or_abort', below, for syntax
 #  - Hopefully, if gcc is present, then all associated tools will be
-#  - awk must be GNU awk
 #  - makeinfo for building docs, even if discarded later on
 #  - others obvious... :-/
 #
@@ -44,7 +43,7 @@ xargs
 install:install=GNU coreutils
 make:make=^GNU Make
 gcc
-awk:awk=^GNU Awk || gawk=^GNU Awk
+awk
 bison
 flex
 makeinfo