aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1999-12-16 15:25:14 +0000
committerDavid Aspinall1999-12-16 15:25:14 +0000
commita5aa9769a19e99fe4edec321c0628ed8eadf6c59 (patch)
tree23daaedeac2c94970ab2680d94c14bbdbb8f9650 /doc
parentc1a0354d0679fd172b70b4568a452ae9f13121ab (diff)
Typos.
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi7
1 files 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}.