diff options
| author | Enrico Tassi | 2014-11-27 15:44:16 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-11-27 16:06:54 +0100 |
| commit | b9b3935191cae5c1d8b592742ea46a2e1b525ded (patch) | |
| tree | bb782d3cc694564f31ec01c500d88f25ed1fe3d5 /lib | |
| parent | df8779378c3ea30f90b11204828c3a33513b9e3d (diff) | |
better to always print the thread id
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/system.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/lib/system.ml b/lib/system.ml index b0b5aa1a8c..0c4e892b9e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -260,7 +260,5 @@ let with_time time f x = 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" + else Printf.sprintf "master:%d" (Thread.id (Thread.self ())) |