diff -r 7ac43d3747c0 -r 3448ac3f1a5d configure
--- a/configure	Mon Apr 20 20:14:53 2009 +0000
+++ b/configure	Mon Apr 20 21:10:03 2009 +0000
@@ -4,9 +4,8 @@
 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 @@
 install:install=GNU coreutils
 make:make=^GNU Make
 gcc
-awk:awk=^GNU Awk || gawk=^GNU Awk
+awk
 bison
 flex
 makeinfo