Make absence of makeinfo a fatal error only if the info files don't exist.
authorGlenn Morris <rgm@gnu.org>
Fri, 9 May 2008 04:27:56 +0000 (04:27 +0000)
committerGlenn Morris <rgm@gnu.org>
Fri, 9 May 2008 04:27:56 +0000 (04:27 +0000)
commit09817afc31700d6611e78eb88c67710124f7c881
tree85d275a3f1a6a61d77b69d0d0ed398f33074e19c
parent8275fb5af0e53b66d6e1348777f817e0a175088b
Make absence of makeinfo a fatal error only if the info files don't exist.
configure.in