(--without-makeinfo): New option. If set, absence of suitable
commit4c18f8b45c81f17023dd2f5e99850dfde73ab047
authorGlenn Morris <rgm@gnu.org>
Sat, 3 May 2008 20:16:15 +0000 (3 20:16 +0000)
committerGlenn Morris <rgm@gnu.org>
Sat, 3 May 2008 20:16:15 +0000 (3 20:16 +0000)
tree800a8fcf93a81416e69d800444701a105e943ed4
parent175aea10f7d01f138993539274cd71ddf75a0b48
(--without-makeinfo): New option.  If set, absence of suitable
makeinfo is not a fatal error.
configure.in