From f2fb98eabdb2f550c177609ad70ab8ba57821bca Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 29 Aug 2016 10:52:34 +0200 Subject: Send Dependency feedback only if file not already loaded. --- library/library.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/library.ml') 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 -- cgit v1.2.3