diff options
Diffstat (limited to 'lib/system.ml')
| -rw-r--r-- | lib/system.ml | 7 |
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" + |
