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
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::