From fae1e1bb8de23d84b13d8e36e183a4147d404b25 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jan 2019 10:40:42 +0100
Subject: [checker] avoid some printing in non verbose mode

---
 checker/check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/checker/check.ml b/checker/check.ml
index 30437e8bd0..b2930d9535 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -329,7 +329,7 @@ let intern_from_file (dir, f) =
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
-       chk_pp (str " (was a vio file) ");
+       Flags.if_verbose chk_pp (str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
         user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
-- 
cgit v1.2.3