This should have ideally been part of earlier commit v1.12.1-93-g3c64d54.
* defs (makeinfo-html): Remove.
Signed-off-by: Stefano Lattarini <stefano.lattar...@gmail.com>
---
defs | 7 -------
1 file changed, 7 deletions(-)
diff --git a/defs b/defs
index a6d2b4a..0b01f59 100644
--- a/defs
+++ b/defs
@@ -854,13 +854,6 @@ do
makedepend -f- \
|| skip_all_ "required program 'makedepend' not available"
;;
- makeinfo-html)
- # Make sure we have makeinfo, and it understands '--html'.
- echo "$me: running makeinfo --html --version"
- makeinfo --html --version \
- || skip_all_ "cannot find a makeinfo program that groks" \
- "the '--html' option"
- ;;
mingw)
uname_s=`uname -s || echo UNKNOWN`
echo "$me: system name: $uname_s"
--
1.7.9.5
