configure
changeset 1299 3448ac3f1a5d
parent 1298 7ac43d3747c0
child 1302 7df725fc8f66
     1.1 --- a/configure	Mon Apr 20 20:14:53 2009 +0000
     1.2 +++ b/configure	Mon Apr 20 21:10:03 2009 +0000
     1.3 @@ -4,9 +4,8 @@
     1.4  DATE=$( date +%Y%m%d )
     1.5  
     1.6  # All absolutely required tools, one per line to ease diff.
     1.7 -# See function 'has_or_abort, below, for syntax
     1.8 +# See function 'has_or_abort', below, for syntax
     1.9  #  - Hopefully, if gcc is present, then all associated tools will be
    1.10 -#  - awk must be GNU awk
    1.11  #  - makeinfo for building docs, even if discarded later on
    1.12  #  - others obvious... :-/
    1.13  #
    1.14 @@ -44,7 +43,7 @@
    1.15  install:install=GNU coreutils
    1.16  make:make=^GNU Make
    1.17  gcc
    1.18 -awk:awk=^GNU Awk || gawk=^GNU Awk
    1.19 +awk
    1.20  bison
    1.21  flex
    1.22  makeinfo