aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-12-13 23:57:43 +0100
committerMaxime Dénès2017-12-13 23:57:43 +0100
commit671c4dbd064884a042d8f2bea5186ab5c7eaaeec (patch)
tree5b96358dbceed10a46fa42ecde293c0fe8d6ce7a /lib/system.ml
parentb1aaedb9e728702cccdb1bd126a714d9e075d14c (diff)
parent50159f9c1748ccf1d66341d171081a998d116d2f (diff)
Merge PR #1108: [stm] Reorganize flags
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 4b5066ef41..2c8dbac7c0 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,9 +309,3 @@ let with_time time f x =
let msg2 = if time then "" else " (failure)" in
Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
-
-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 ()))