aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-04-21 17:43:01 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-04-21 17:43:08 +0200
commit2a5fd12d597d4337810ae367ea3a49720ee3d80c (patch)
treedb33e0258a98e5e9715d0d2dc0bd4ecd3629b77c /stm
parenta45bd5981092cceefc4d4d30f9be327bb69c22d8 (diff)
STM: print trace on "anomaly, no safe id attached"
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 38745e227..f36b757f2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2018,7 +2018,7 @@ let handle_failure (e, info) vcs tty =
end;
VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
- Errors.print_no_report e)
+ Errors.iprint_no_report (e, info))
| Some (safe_id, id) ->
prerr_endline ("Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;