From 5bb74282037a34098408ab3d01e9a11318cb8351 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Tue, 17 Jan 2017 16:19:33 +0100
Subject: use makeinfo instead of texi2html

texi2html is dead, see for instance
https://wiki.debian.org/Texi2htmlTransition
---
 doc/Makefile.doc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index b5eb4d82..b2e69d53 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -18,7 +18,7 @@
 
 MAKE = make -f Makefile.doc 
 MAKEINFO = makeinfo
-TEXI2HTML = texi2html -expandinfo -number-sections -split_chapter --noheader --css-include proofgen.css
+TEXI2HTML = makeinfo --html --ifinfo --number-sections --split=chapter --no-headers --css-include=proofgen.css
 # `texinfo-tex' package contains texi2pdf
 TEXI2PDF = texi2pdf
 # `dviutils' package contains these useful utilities.
@@ -50,7 +50,7 @@ default: doc
 	$(TEXI2PDF) $< 
 
 .texi.html:	
-	$(TEXI2HTML) --output $* $< 
+	$(TEXI2HTML) $<
 
 default: doc
 
-- 
cgit v1.2.3