diff options
| author | David Aspinall | 1999-12-16 15:25:14 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-12-16 15:25:14 +0000 |
| commit | a5aa9769a19e99fe4edec321c0628ed8eadf6c59 (patch) | |
| tree | 23daaedeac2c94970ab2680d94c14bbdbb8f9650 | |
| parent | c1a0354d0679fd172b70b4568a452ae9f13121ab (diff) | |
Typos.
| -rw-r--r-- | doc/ProofGeneral.texi | 7 |
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}. |