From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:03:54 +0200
Subject: Remove uses of [Flags.make_silent]

---
 checker/checker.ml | 2 +-
 checker/include    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 57e1806cff..5cadfe7b94 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -354,7 +354,7 @@ let parse_args argv =
     | "-norec" :: [] -> usage ()
 
     | "-silent" :: rem ->
-        Flags.make_silent true; parse rem
+        Flags.quiet := true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
         fatal_error (str "Unknown option " ++ str s) false
diff --git a/checker/include b/checker/include
index 6bea3c91a7..09bf2826c0 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