aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2013-07-17 10:38:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2013-07-17 10:38:52 +0000
commit6ba6a73bb719ebb99065747cf07c9f9066e299a7 (patch)
treeb278d0e0afafe99b740d21947ee60d35bcbf723f /doc
parent9246e607dc5fa1b2d26a308eb44541018034cb0c (diff)
Fix image name
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 f843b9e2..96507f05 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -91,7 +91,7 @@ END-INFO-DIR-ENTRY
@iftex
@vskip 1cm
-@image{ProofGeneral}
+@image{ProofGeneral-image}
@end iftex
@author David Aspinall with T. Kleymann
@page