configure
changeset 1431 28a90ba877ca
parent 1430 933eee133cbf
child 1432 76f8feef64c4
     1.1 --- a/configure	Wed Jul 15 09:22:47 2009 +0200
     1.2 +++ b/configure	Wed Jul 22 20:42:23 2009 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4               ver='^GNU Make (3.[89][[:digit:]]|[4-9])'  \
     1.5               err="GNU 'make' 3.80 or above was not found"
     1.6  has_or_abort prog=gcc
     1.7 -has_or_abort prog=awk
     1.8 +has_or_abort prog="awk gawk" ver='^GNU Awk' err="GNU 'awk' was not found"
     1.9  has_or_abort prog=bison
    1.10  has_or_abort prog=flex
    1.11  has_or_abort prog=makeinfo