diff --git a/configure b/configure index d832593ac977b261feff3442595a2a810f8dc43e..084c161d1735208a549e35df84fbba23a1c8aa17 100755 --- a/configure +++ b/configure @@ -3726,6 +3726,9 @@ echo "openal enabled ${openal-no}" echo "openssl enabled ${openssl-no}" echo "zlib enabled ${zlib-no}" echo "bzlib enabled ${bzlib-no}" +echo "texi2html enabled ${texi2html-no}" +echo "pod2man enabled ${pod2man-no}" +echo "makeinfo enabled ${makeinfo-no}" test -n "$random_seed" && echo "random seed ${random_seed}" echo