Skip to content

Commit

Permalink
doc/ProofGeneral.texi: fix makeinfo
Browse files Browse the repository at this point in the history
Fixes the following error:

node `Coq Proof General' lacks menu item for `Proof using annotations' despite being its Up target
  • Loading branch information
Toni Dietze committed May 6, 2020
1 parent 24e1c5a commit 9bd6175
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions doc/ProofGeneral.texi
Original file line number Diff line number Diff line change
Expand Up @@ -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::
Expand Down

0 comments on commit 9bd6175

Please sign in to comment.