From 0a79658cc7d0278f0aeaf72ff24688346f5b3fde Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 8 Oct 1998 11:20:41 +0000
Subject: Removed mysterious @ignores around info dir entry.

---
 doc/ProofGeneral.texi | 2 --
 1 file changed, 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
 
-- 
cgit v1.2.3