diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 08:45:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 11:39:12 +0100 |
| commit | 21a1c8abdd5807427849c34875c294cb6ad7d899 (patch) | |
| tree | 3a722cc770663196bb23ad37c36bd23fff1a41bd /tools/coqdep_common.ml | |
| parent | 34bb77c953e917f5fbff489c5758abcbadc22224 (diff) | |
coqdep: Warning about ml file clashes, keeping the file corresponding
to the first -I option.
Fortunately, with -I option, only one file can be found by occurrence
of the option, so on the contrary of -Q/-R options for v files, the
order is not file-system dependent.
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d7532dba6..25fd49082 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -103,9 +103,17 @@ let safe_hash_add clq q (k,v) = For the ML files, the string is the basename without extension. *) +let warning_ml_clash x s s' suff = + eprintf + "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff + (match s with None -> "." | Some d -> d) + ((match s' with None -> "." | Some d -> d) // x) suff + let mkknown () = let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in - let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s + let add x s suff = + try let s' = Hashtbl.find h x in warning_ml_clash x s' s suff + with Not_found -> Hashtbl.add h x s and iter f = Hashtbl.iter f h and search x = try Some (Hashtbl.find h x) @@ -428,11 +436,13 @@ let rec suffixes = function | dir::suffix as l -> l::suffixes suffix let add_caml_known phys_dir _ f = - match get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] with - | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir) - | (basename,".mli") -> add_mli_known basename (Some phys_dir) - | (basename,".mllib") -> add_mllib_known basename (Some phys_dir) - | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir) + let basename,suff = + get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in + match suff with + | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff + | ".mli" -> add_mli_known basename (Some phys_dir) suff + | ".mllib" -> add_mllib_known basename (Some phys_dir) suff + | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff | _ -> () let add_known recur phys_dir log_dir f = |