aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-08-29 10:52:34 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-08-29 10:54:38 +0200
commitf2fb98eabdb2f550c177609ad70ab8ba57821bca (patch)
tree8c645e8919f9a13c073c3ea518a1cd4768af304e /library/library.ml
parent812712c0683d03760c10ef7397fb4ff0041c4860 (diff)
Send Dependency feedback only if file not already loaded.
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 04b82f2f3..4bd71888e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -452,13 +452,13 @@ let intern_from_file f =
module DPMap = Map.Make(DirPath)
let rec intern_library (needed, contents) (dir, f) from =
- Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
(* Look if already listed and consequently its dependencies too *)
try (DPMap.find dir contents).library_digests, (needed, contents)
with Not_found ->
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in