From 9bd6175a864dbaebce49c49416651b6532a9f7ee Mon Sep 17 00:00:00 2001
From: Toni Dietze <>
Date: Wed, 6 May 2020 13:49:23 +0200
Subject: [PATCH 1/2] doc/ProofGeneral.texi: fix makeinfo

Fixes the following error:

node `Coq Proof General' lacks menu item for `Proof using annotations' despite being its Up target
---
 doc/ProofGeneral.texi | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 24d4d7e81..dfa09085d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4294,6 +4294,7 @@ assistant.  It supports most of the generic features of Proof General.
 @menu
 * Coq-specific commands::
 * Using the Coq project file::
+* Proof using annotations::
 * Multiple File Support::
 * Editing multiple proofs::
 * User-loaded tactics::

From c3304c49c9d3c1c304e64e34b85ee032b28f3cbe Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik@martin-dorel.org>
Date: Wed, 6 May 2020 21:20:28 +0200
Subject: [PATCH 2/2] test: Add CI step to build the doc

* Only build the info manual.

* Otherwise we would get the following issue:

$ texi2pdf PG-adapting.texi
You don't have a working TeX binary (tex) installed anywhere in
your PATH, and texi2dvi cannot proceed without one.  If you want to use
this script, you'll need to install TeX (if you don't have it) or change
your PATH or TEX environment variable (if you do).  See the --help
output for more details.

For information about obtaining TeX, please see http://tug.org/texlive,
Makefile.doc:50: recipe for target 'PG-adapting.pdf' failed
or do a web search for TeX and your operating system or distro.

On Debian you can install a working TeX system with
  apt-get install texlive
---
 .github/workflows/test.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index db4bb766c..6f67a0f43 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -41,6 +41,9 @@ jobs:
 
     - run: emacs --version
     - run: make
+    - name: Install makeinfo
+      run: sudo apt-get update -y -q && sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends texinfo
+    - run: make doc.info
 
   test:
     runs-on: ubuntu-latest