diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 16:42:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-18 16:42:43 +0000 |
| commit | a66a16e2e1d3264d87eaac66a809ec5e26849044 (patch) | |
| tree | a76c0722da5be97c388baba8c0b864de8c1e1b7c /tools | |
| parent | f418ecb6a2915a8b8b9fd5598ced5376cbcb75bc (diff) | |
Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in
coqdep since it is now deterministic (later -R's overwriting former ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 797c25ccc..a2d908339 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -137,7 +137,7 @@ let warning_clash file dir = let d2 = Filename.dirname f2 in let dl = List.map Filename.dirname (List.rev fl) in eprintf - "*** Warning: in file %s, \n required library %s is ambiguous!\n (found %s.v in " + "*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in " file (String.concat "." dir) f; List.iter (fun s -> eprintf "%s, " s) dl; eprintf "%s and %s; used the latter)\n" d2 d1 |