diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /checker/check.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'checker/check.ml')
-rw-r--r-- | checker/check.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/check.ml b/checker/check.ml index 40ac604e..82df62b4 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -211,7 +211,7 @@ let locate_absolute_library dir = if loadpath = [] then raise LibUnmappedDir; try let name = string_of_id base^".vo" in - let _, file = System.where_in_path false loadpath name in + let _, file = System.where_in_path ~warn:false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -231,7 +231,7 @@ let locate_qualified_library qid = in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in - let path, file = System.where_in_path true loadpath name in + let path, file = System.where_in_path loadpath name in let dir = extend_dirpath (find_logical_path path) (id_of_string qid.basename) in (* Look if loaded *) |