Add the option to build Texinfo-format documentation.

Bug-Debian: https://bugs.debian.org/881959
Last-Update: 2017-11-27

Gbp-Pq: Name doc-build-texinfo.diff

diff --git a/Doc/Makefile b/Doc/Makefile
index 57763fc0e103d753f7a3135eee5205ac68d5b499..c309c0f7d05dcfa3f35c2720cf401c11b4b5533d 100644 (file)
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -32,6 +32,7 @@ help:
        @echo "  htmlview   to open the index page built by the html target in your browser"
        @echo "  htmlhelp   to make HTML files and a HTML help project"
        @echo "  latex      to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
+       @echo "  texinfo    to make Texinfo files"
        @echo "  text       to make plain text files"
        @echo "  texinfo    to make Texinfo file"
        @echo "  epub       to make EPUB files"
@@ -86,6 +87,11 @@ latex: build
        @echo "Run \`make all-pdf' or \`make all-ps' in that directory to" \
              "run these through (pdf)latex."
 
+texinfo: BUILDER = texinfo
+texinfo: build
+       @echo "Build finished; the Texinfo files are in build/texinfo."
+       @echo "Run \`make\' in that directory to run these through makeinfo."
+
 text: BUILDER = text
 text: build
        @echo "Build finished; the text files are in build/text."