aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-15 17:36:14 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-15 17:36:14 +0200
commit7385d3c7fc6b3bd7101e6a7ce5ff00008e187e89 (patch)
treeee6d1319933575139bd535ecf07090e6dd30a570 /plugins
parent8e9042fa46e67f686de9b917c6dbcf49d585c38c (diff)
ssrmatching: debug prints sent via msg_debug
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 718296c50..4cb8837a2 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -61,7 +61,7 @@ let ppnl = Feedback.msg_info
(* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
(* or if SsrDebug is Set *)
let pp_ref = ref (fun _ -> ())
-let ssr_pp s = Feedback.msg_error (str"SSR: "++Lazy.force s)
+let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s)
let _ =
try ignore(Sys.getenv "SSRMATCHINGDEBUG"); pp_ref := ssr_pp
with Not_found -> ()