aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorMaxime Dénès2019-08-02 16:47:49 +0200
committerMaxime Dénès2019-08-29 10:27:04 +0200
commit6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 (patch)
tree8ea8af9ee03d627126de323898ce73d3a43e608e /lib
parent1e6fb6005ef98d1709b09adfcb0726da2fc8b7f4 (diff)
Make sure that all query commands return a notice (not an info) feedback
As documented in the feedback API.
Diffstat (limited to 'lib')
-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 *)