aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/spawned.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/spawned.ml')
-rw-r--r--stm/spawned.ml6
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 ()))