aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
authorMaxime Dénès2019-08-02 16:07:43 +0200
committerMaxime Dénès2019-08-29 10:27:01 +0200
commit3e339284060b4fb3ca6d5c86e354615a4941eca9 (patch)
treeee3371db9ea3bdf92172054d13c26b14ee7bfaee /engine
parent1ab00ddd8fa6ca5428c7f6ff56de0562bcb4ca1f (diff)
Logic monad debug printer now emits a debug message
Diffstat (limited to 'engine')
-rw-r--r--engine/logic_monad.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 7c06bb59f1..bada18feff 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -108,7 +108,7 @@ struct
Util.iraise (Exception e, info)
(** Use the current logger. The buffer is also flushed. *)
- let print_debug s = make (fun _ -> Feedback.msg_info s)
+ let print_debug s = make (fun _ -> Feedback.msg_debug s)
let print_info s = make (fun _ -> Feedback.msg_info s)
let print_warning s = make (fun _ -> Feedback.msg_warning s)
let print_notice s = make (fun _ -> Feedback.msg_notice s)