diff options
| author | Pierre-Marie Pédrot | 2020-04-09 12:58:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-09 12:58:14 +0200 |
| commit | d233c495821f5090b9dd37eec5ed07930f66b561 (patch) | |
| tree | 0ef9f8d7c198df86ff48c9dc22458a2119169f3d /tools | |
| parent | 3778576937512bf9deed90de7b5aad75ef5cde13 (diff) | |
| parent | f06d96687e26d3e491de0a234e889e901b32e1ca (diff) | |
Merge PR #12050: Fix a typo in CoqMakefile.in
Reviewed-by: ppedrot
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). |