From b43676541010546b9d41281c1689c242511fa39e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Tue, 22 Oct 2013 09:22:09 +0000
Subject: New feedback message: SlaveStatus

To tell the gui what a slave is doing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/interface.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/interface.mli')

diff --git a/lib/interface.mli b/lib/interface.mli
index 69eaac7890..a8e3d72bd1 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -126,6 +126,7 @@ type feedback_content =
   | GlobRef of Loc.t * string * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
+  | SlaveStatus of int * string
 
 type feedback = {
   id : edit_or_state_id;
-- 
cgit v1.2.3