From b35edb34769fecd4dbdf7030222ba3078eab1c93 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Apr 2014 13:59:39 +0200
Subject: Fixing various backtrace recordings.

---
 kernel/safe_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e9be955e82..c89766fb9b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -688,7 +688,9 @@ let export compilation_mode senv dir =
     try
       if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
       else join_safe_environment senv
-    with e -> Errors.errorlabstrm "export" (Errors.print e)
+    with e ->
+      let e = Errors.push e in
+      Errors.errorlabstrm "export" (Errors.print e)
   in
   assert(senv.future_cst = []);
   let () = check_current_library dir senv in
-- 
cgit v1.2.3