diff options
| author | Pierre-Marie Pédrot | 2014-04-25 13:59:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-25 14:00:43 +0200 |
| commit | b35edb34769fecd4dbdf7030222ba3078eab1c93 (patch) | |
| tree | 0efb56c5711b0a2d9ae8eef5b7792b734899f2be /kernel | |
| parent | a5e0b28f9344744edf2209001fe047b1535775f6 (diff) | |
Fixing various backtrace recordings.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |