aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/feedback.mli')
-rw-r--r--lib/feedback.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli
index e7645ca16..c245ec76a 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;