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 /tools/coqdep_common.ml | |
| parent | 046657081fb769fcf033c7d7c6b3fb6e861a0996 (diff) | |
coqdep: remove optimization making makefiles harder to write
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 = |