aboutsummaryrefslogtreecommitdiff
path: root/lib/system.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-09-04 15:00:03 +0200
committerEmilio Jesus Gallego Arias2019-09-04 15:00:03 +0200
commit6a6a2575c10d05cd0151a83c133825d43bd3cb28 (patch)
treea46211ebfa7af615d7edd8359208f8e5dcd5af1d /lib/system.ml
parentbcf2dae1e39c6ff27c574a82c4451323a673b15f (diff)
parent2d4033152c51eb0b093c79d19a5146995af1b432 (diff)
Merge PR #10612: Fix feedback levels
Ack-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'lib/system.ml')
-rw-r--r--lib/system.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/system.ml b/lib/system.ml
index b1a9efccfc..8c333ec267 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -300,13 +300,13 @@ let with_time ~batch ~header f x =
let y = f x in
let tend = get_time() in
let msg2 = if batch then "" else " (successful)" in
- Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
y
with e ->
let tend = get_time() in
let msg = if batch then "" else "Finished failing transaction in " in
let msg2 = if batch then "" else " (failure)" in
- Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
(* We use argv.[0] as we don't want to resolve symlinks *)