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
---
 lib/feedback.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index e7645ca169..c245ec76a1 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -24,6 +24,8 @@ type feedback_content =
   | InProgress of int
   | SlaveStatus of int * string
   | ProcessingInMaster
+  | Goals of Loc.t * string
+  | FileLoaded of string * string
 
 type feedback = {
   id : edit_or_state_id;
-- 
cgit v1.2.3