From f202e65fc3542295247dff380c1b02ad11c2ec8f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 13 Sep 2000 18:00:52 +0000
Subject: Removed keystroke index.

---
 doc/PG-adapting.texi | 1 -
 1 file changed, 1 deletion(-)

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 34605081..12087979 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -176,7 +176,6 @@ Proof General.
 * Demonstration Instantiations::
 * Function Index::              
 * Variable Index::              
-* Keystroke Index::             
 * Concept Index::               
 @end menu
 @end ifinfo
-- 
cgit v1.2.3