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

---
 stm/workerPool.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm/workerPool.mli')

diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index d7a546929..d55b35c28 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -13,13 +13,14 @@ module Make(Worker : sig
       process * in_channel * out_channel
 end) : sig
 
-type worker_id = int
+type worker_id = string
 type spawn =
   args:string array -> env:string array -> unit ->
     in_channel * out_channel * Worker.process
 
 val init :
-  size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> unit
+  size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) ->
+  (int -> worker_id) -> unit
 val is_empty : unit -> bool
 val n_workers : unit -> int
 val cancel : worker_id -> unit
-- 
cgit v1.2.3