diff options
| author | Maxime Dénès | 2017-12-13 23:57:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-13 23:57:43 +0100 |
| commit | 671c4dbd064884a042d8f2bea5186ab5c7eaaeec (patch) | |
| tree | 5b96358dbceed10a46fa42ecde293c0fe8d6ce7a /stm/spawned.ml | |
| parent | b1aaedb9e728702cccdb1bd126a714d9e075d14c (diff) | |
| parent | 50159f9c1748ccf1d66341d171081a998d116d2f (diff) | |
Merge PR #1108: [stm] Reorganize flags
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 6ab096abf9..fb5708f3a3 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 ())) |