diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-01-17 10:35:09 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-23 10:48:28 +0200 |
commit | 4252789c77479b9d4a9ac5a12e9a24067b086040 (patch) | |
tree | fa3546e9371f4aa50bdaf92333d52a54a0af1472 | |
parent | 046657081fb769fcf033c7d7c6b3fb6e861a0996 (diff) |
coqdep: remove optimization making makefiles harder to write
-rw-r--r-- | tools/coqdep.ml | 2 | ||||
-rw-r--r-- | tools/coqdep_common.ml | 1 |
2 files changed, 1 insertions, 2 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"; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 281644d23..6e7935d09 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -219,7 +219,6 @@ let register_dir_logpath,find_dir_logpath = let file_name s = function | None -> s - | Some "." -> s | Some d -> d // s let depend_ML str = |