From 2a805fd99b96746dbfe381d64cd7eaba84fdca79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jul 2014 15:59:44 +0200
Subject: Feedback: LoadedFile + Goals

LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
---
 library/library.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 4f023ce6df..9552a6ca9b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,6 +488,7 @@ let rec intern_library (needed, contents) (dir, f) =
       (str ("The file " ^ f ^ " contains library") ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
+  Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f));
   m, intern_library_deps (needed, contents) dir m
 
 and intern_library_deps libs dir m =
-- 
cgit v1.2.3