aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 4188eb2b4a..59260fbf63 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -295,3 +295,10 @@ let with_time time f x =
let msg2 = if time then "" else " (failure)" in
msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
+
+let process_id () =
+ if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+ else if Flags.async_proofs_is_master () then
+ Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
+ else "master"
+