diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 76ead853..f5963679 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -8,7 +8,6 @@ @paragraphindent 0 @c %**end of header -@ignore @ifinfo @format START-INFO-DIR-ENTRY @@ -16,7 +15,6 @@ START-INFO-DIR-ENTRY END-INFO-DIR-ENTRY @end format @end ifinfo -@end ignore @setchapternewpage odd |