From a5aa9769a19e99fe4edec321c0628ed8eadf6c59 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 16 Dec 1999 15:25:14 +0000
Subject: Typos.

---
 doc/ProofGeneral.texi | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 3e128f07..ec7a9417 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1959,7 +1959,7 @@ file. On the contrary with this method, Emacs will do this operation
 automatically.
 
 Extending the previous example, if the makefile for @file{foo.v} is
-located in directory @file{.../dir/}, you can add the good compile
+located in directory @file{.../dir/}, you can add the right compile
 command:
 
 @lisp
@@ -1971,10 +1971,11 @@ command:
 *)
 @end lisp
 
-And then the good call to makefile will be done if you use the @kbd{M-x
+And then the right call to make will be done if you use the @kbd{M-x
 compile} command. Notice that the lines are commented in order to be
 ignored by the proof assistant. It is possible to use this mechanism for
-any other buffer local variable. Read (@inforef{File Variables, ,xemacs}.
+any other buffer local variable. Read (@inforef{File Variables,
+,xemacs}.
 
 
 
-- 
cgit v1.2.3