diff options
| author | David Aspinall | 2000-09-21 18:21:40 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-09-21 18:21:40 +0000 |
| commit | 38fa200b96a42e31e70cb8533d09ac90aa66655a (patch) | |
| tree | 1d36273b14a647c20c82763db1feeec42ce23250 /doc | |
| parent | 7f2c0f5a2c0d60480df7131c380c92c7c63467fc (diff) | |
Slightly shorter name for info dir entry.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 03e7926b..f6cb3a40 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -68,7 +68,7 @@ @ifinfo @format START-INFO-DIR-ENTRY -* Adapting Proof General: (PG-adapting). How to adapt Proof General for new provers +* Adapting PG: (PG-adapting). How to adapt Proof General for new provers END-INFO-DIR-ENTRY @end format @end ifinfo |