aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tools/coqdep.ml2
-rw-r--r--tools/coqdep_common.ml1
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 =