From e162aa587ea9be86ae6a9d2c6c11560137f17e73 Mon Sep 17 00:00:00 2001
From: notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 22 Mar 2007 10:31:13 +0000
Subject: Correction des bugs #1455 et #1456

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9728 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/cdglobals.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'tools/coqdoc/cdglobals.ml')

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index c5abbff05..eef598fdd 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -29,16 +29,11 @@ let open_out_file f =
   let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in
     out_channel := open_out f
 
-let open_temp_out_file prefix suffix =
-  let tmp_fname, tmp_ochan = Filename.open_temp_file prefix suffix in
-    out_channel := tmp_ochan;
-    tmp_fname
-
 let close_out_file () = close_out !out_channel
 
 
 let header_trailer = ref true
-let quiet = ref false
+let quiet = ref true
 let light = ref false
 let gallina = ref false
 let short = ref false
-- 
cgit v1.2.3