diff options
author | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
commit | 234f5479773d43a48e67c5c0ea361445c7fb6782 (patch) | |
tree | 0609f0aef4769561d3bee2049c5c973f40b20be3 /tools/coq_makefile.ml | |
parent | 32415df7e24d4d79a00fae95a5f619980b006c61 (diff) |
Correct some spelling errorsmaster
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ad489da82..33ced97ed 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -48,7 +48,7 @@ let usage_common () = \n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ \n as a dependencies of an already defined target \"foo\".\ \n[-I dir]: look for Objective Caml dependencies in \"dir\"\ -\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n[-R physicalpath logicalpath]: look for Coq dependencies recursively\ \n starting from \"physicalpath\". The logical path associated to the\ \n physical path is \"logicalpath\".\ \n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ |