summaryrefslogtreecommitdiff
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /tools/coqdep_common.ml
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c4e8b23c..0961e398 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -138,7 +138,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