aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-05-08 14:59:38 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-05-08 14:59:38 +0000
commit6284f4b093e82e9e3fd8df1dd41ad6a752761271 (patch)
tree322a51894bd70946e47eaf6641fc7c41c0f1eda4 /doc
parent19afa4e1abcc6dc37b94545825c5507674bc4380 (diff)
Change info dir entry to appear next to Proof General entry.
Diffstat (limited to 'doc')
-rw-r--r--doc/PG-adapting.texi2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index a7ced8f1..b63de126 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -68,7 +68,7 @@
@ifinfo
@format
START-INFO-DIR-ENTRY
-* Adapting PG: (PG-adapting). How to adapt Proof General for new provers
+* Proof General Adapting: (PG-adapting). How to adapt Proof General for new provers
END-INFO-DIR-ENTRY
@end format
@end ifinfo