From 4e724634839726aa11534f16e4bfb95cd81232a4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 23 Jul 2014 11:54:36 +0200
Subject: STM: code restructured to reuse task queue for tactics

---
 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 b3c0c8896..7e7b57625 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -40,7 +40,7 @@ type feedback_content =
   | GlobDef of Loc.t * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
-  | SlaveStatus of int * string
+  | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
   | FileLoaded of string * string
-- 
cgit v1.2.3