diff options
| author | Enrico Tassi | 2014-07-23 11:54:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-08-05 18:24:50 +0200 |
| commit | 4e724634839726aa11534f16e4bfb95cd81232a4 (patch) | |
| tree | 2114ba0a78c4df764d78ad260e30f5fa6854df95 /stm/workerPool.mli | |
| parent | 95e97b68744eeb8bf20811c3938d78912eb3e918 (diff) | |
STM: code restructured to reuse task queue for tactics
Diffstat (limited to 'stm/workerPool.mli')
| -rw-r--r-- | stm/workerPool.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/stm/workerPool.mli b/stm/workerPool.mli index d7a546929f..d55b35c282 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 |