diff options
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 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 |