diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 04:12:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 11:59:07 +0100 |
| commit | a758aac39aa330911f5f589ab3cae1bebed1e9ce (patch) | |
| tree | 17e8e7c41a194a8ac3d17c9fa922da1177e574d4 /stm/spawned.ml | |
| parent | a77f3a3e076e273af35ad520cae2eef0e3552811 (diff) | |
[stm] Move process_id to Spawned.
This brings us one step closer to actually moving all STM flags to
`stm`.
Diffstat (limited to 'stm/spawned.ml')
| -rw-r--r-- | stm/spawned.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml index 6ab096abf..fb5708f3a 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -73,3 +73,9 @@ let get_channels () = Printf.eprintf "Fatal error: ideslave communication channels not set.\n"; exit 1 | Some(ic, oc) -> ic, oc + +let process_id () = + Printf.sprintf "%d:%s:%d" (Unix.getpid ()) + (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else "master") + (Thread.id (Thread.self ())) |