aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-17 10:35:09 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commit4252789c77479b9d4a9ac5a12e9a24067b086040 (patch)
treefa3546e9371f4aa50bdaf92333d52a54a0af1472 /tools/coqdep.ml
parent046657081fb769fcf033c7d7c6b3fb6e861a0996 (diff)
coqdep: remove optimization making makefiles harder to write
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 1c1c1be6a..930b092d3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -435,7 +435,7 @@ let usage () =
ML Module\" commands in coq files.\n"; *)
(* Does not work anymore: *)
(* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *)
- eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n";
+ eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
eprintf " -sort : output the given file name ordered by dependencies\n";
eprintf " -noglob | -no-glob : \n";
eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n";