From 893ea5219eb74aedf93bd53f23b5e050fb9acbf6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 25 Jun 2016 16:05:25 +0200
Subject: [feedback] Allow messages to carry a location.

The new warnings mechanism may which to forward a location to
IDEs. This also makes sense for other message types.

Next step is to remove redundant MsgError feedback type.
---
 lib/feedback.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 7b293ae30..36fb3867f 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -46,7 +46,7 @@ type feedback_content =
   (* Extra metadata *)
   | Custom of Loc.t * string * xml
   (* Old generic messages *)
-  | Message of level * Richpp.richpp
+  | Message of level * Loc.t option * Richpp.richpp
 
 type feedback = {
   id       : edit_or_state_id;  (* The document part concerned *)
-- 
cgit v1.2.3