From 4252789c77479b9d4a9ac5a12e9a24067b086040 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 17 Jan 2017 10:35:09 +0100
Subject: coqdep: remove optimization making makefiles harder to write

---
 tools/coqdep.ml        | 2 +-
 tools/coqdep_common.ml | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 1c1c1be6aa..930b092d3b 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 281644d23e..6e7935d099 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 =
-- 
cgit v1.2.3