diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f72b99c57c..597351db9b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -54,7 +54,7 @@ OCAMLWARN := $(COQMF_WARN) # # Parameters are make variable assignments. # They can be passed to (each call to) make on the command line. -# They can also be put in @LOCAL_FILE@ once an for all. +# They can also be put in @LOCAL_FILE@ once and for all. # For retro-compatibility reasons they can be put in the _CoqProject, but this # practice is discouraged since _CoqProject better not contain make specific # code (be nice to user interfaces). |