Skip to content
Snippets Groups Projects
Commit 1fd922af authored by David Bühler's avatar David Bühler
Browse files

[kernel] Option -save always saves the session on errors.

With a suffix to the saved file name depending on the error:
- ".break" on user interruption
- ".error" on user error
- ".crash" otherwise.
parent 0b6c3dd4
No related branches found
No related tags found
No related merge requests found
...@@ -158,14 +158,14 @@ let save_binary error_extension = ...@@ -158,14 +158,14 @@ let save_binary error_extension =
let () = let () =
(* implement a refinement of the behavior described in BTS #1388: (* implement a refinement of the behavior described in BTS #1388:
- on normal exit: save - on normal exit: save
- on Sys.break, system error or feature request: do not save - on Sys.break (Ctrl-C interruption): save, but add ".break" suffix
- on user error: save, but add ".error" suffix - on user error: save, but add ".error" suffix
- on fatal error or unexpected error: save, but add ".crash" suffix *) - on fatal error or unexpected error: save, but add ".crash" suffix *)
Cmdline.at_normal_exit (fun () -> save_binary None); Cmdline.at_normal_exit (fun () -> save_binary None);
Cmdline.at_error_exit Cmdline.at_error_exit
(function (function
| Sys.Break | Sys_error _ | Log.FeatureRequest _ -> () | Sys.Break -> save_binary (Some ".break")
| Log.AbortError _ -> save_binary (Some ".error") | Log.AbortError _ | Log.FeatureRequest _ -> save_binary (Some ".error")
| _ -> save_binary (Some ".crash")) | _ -> save_binary (Some ".crash"))
(* Write JSON files to disk if required *) (* Write JSON files to disk if required *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment