diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:16 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
| commit | ba30a3da1f41aec6404b49832cdc8516fdcc78ec (patch) | |
| tree | 413ea748445c8e53d20c2dc551cfa6a39ba363f6 /stm | |
| parent | 6129d83ad15799b6b9318a1c4fa5fc73ddbb5ad9 (diff) | |
Marshalling errors should be bold and red (should never happen actually)
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index da2d0fb38..e5e156a4d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -817,7 +817,7 @@ module Task = struct let on_marshal_error s { t_exn_info; t_stop; t_assign; t_loc } = if !fallback_to_lazy_if_marshal_error then begin - msg_warning(strbrk("Marshalling error: "^s^". "^ + msg_error(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here t_exn_info t_loc t_stop)); |