diff options
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 = |