From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Tue, 25 Apr 2017 14:03:54 +0200
Subject: Remove uses of [Flags.make_silent]

---
 checker/include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/include')

diff --git a/checker/include b/checker/include
index 6bea3c91a..09bf2826c 100644
--- a/checker/include
+++ b/checker/include
@@ -116,7 +116,7 @@ let prsub s =
 #install_printer prsub;;*)
 
 Checker.init_with_argv [|"";"-coqlib";"."|];;
-Flags.make_silent false;;
+Flags.quiet := false;;
 Flags.debug := true;;
 Sys.catch_break true;;
 
-- 
cgit v1.2.3