From 0de499ab4702708ddfae162389617869b170c7d7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 28 Sep 2015 16:33:46 +0200
Subject: STM: fix backtrace handling

---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 4a303f036e..ed7c234c1e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1577,7 +1577,8 @@ end = struct (* {{{ *)
       vernac_interp r_for { r_what with verbose = true };
       feedback ~state_id:r_for Feedback.Processed     
     with e when Errors.noncritical e ->
-      let msg = string_of_ppcmds (print e) in
+      let e = Errors.push e in
+      let msg = string_of_ppcmds (iprint e) in
       feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
-- 
cgit v1.2.3