From afbf8601af31b012872a2fae6939be9fd231145f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 4 Nov 2020 16:03:14 +0100
Subject: do not print "refining" unless asked

---
 backend/CSE3analysisaux.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'backend/CSE3analysisaux.ml')

diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
index bd4ca20a..e37ef61f 100644
--- a/backend/CSE3analysisaux.ml
+++ b/backend/CSE3analysisaux.ml
@@ -139,7 +139,8 @@ let refine_invariants
       if not (RB.beq cur nxt)
       then
         begin
-          Printf.printf "refining CSE3 node %d\n" (P.to_int pc);
+          (if !Clflags.option_debug_compcert > 4
+           then Printf.printf "refining CSE3 node %d\n" (P.to_int pc));
           List.iter add_todo (successors pc)
         end in
   (List.iter add_todo nodes);
-- 
cgit