diff options
| author | David Aspinall | 1998-10-08 11:20:41 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-08 11:20:41 +0000 |
| commit | 0a79658cc7d0278f0aeaf72ff24688346f5b3fde (patch) | |
| tree | 67fa6c1253898e9800c51a44026252cfe0995964 /doc | |
| parent | 2313ec66f5493228560c56d9afe390bb208d9d90 (diff) | |
Removed mysterious @ignores around info dir entry.
Diffstat (limited to 'doc')
| -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 |