diff options
| author | Jason Gross | 2020-04-08 11:08:30 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-04-08 11:08:30 -0400 |
| commit | f06d96687e26d3e491de0a234e889e901b32e1ca (patch) | |
| tree | 13d2f37d57b4e875e6f5e65514d8cdd563c1c497 /tools | |
| parent | b26d1f477990d88e235ffda0f23f494456ce5862 (diff) | |
Fix a typo in CoqMakefile.in
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). |