diff -r 933eee133cbf -r 28a90ba877ca configure
--- a/configure	Wed Jul 15 09:22:47 2009 +0200
+++ b/configure	Wed Jul 22 20:42:23 2009 +0200
@@ -327,7 +327,7 @@
              ver='^GNU Make (3.[89][[:digit:]]|[4-9])'  \
              err="GNU 'make' 3.80 or above was not found"
 has_or_abort prog=gcc
-has_or_abort prog=awk
+has_or_abort prog="awk gawk" ver='^GNU Awk' err="GNU 'awk' was not found"
 has_or_abort prog=bison
 has_or_abort prog=flex
 has_or_abort prog=makeinfo