diff options
| author | Pierre-Marie Pédrot | 2014-01-30 15:30:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-30 16:02:33 +0100 |
| commit | 1059ecce2a2662e4d8f335bd4db743df70b100b1 (patch) | |
| tree | 236cad1f42ecaea078f8a0fb17dd17eec81631e0 /lib/backtrace.ml | |
| parent | a5e78ef4a8450991c6f1ee748b720eb0d54d04d2 (diff) | |
Fixing backtrace handling here and there.
Diffstat (limited to 'lib/backtrace.ml')
| -rw-r--r-- | lib/backtrace.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/backtrace.ml b/lib/backtrace.ml index d64f42f7f0..19b07d8767 100644 --- a/lib/backtrace.ml +++ b/lib/backtrace.ml @@ -96,3 +96,16 @@ let add_backtrace e = Exninfo.add e backtrace bt end else e + +let app_backtrace ~src ~dst = + if !is_recording then + match get_backtrace src with + | None -> dst + | Some bt -> + match get_backtrace dst with + | None -> + Exninfo.add dst backtrace bt + | Some nbt -> + let bt = bt @ nbt in + Exninfo.add dst backtrace bt + else dst |