From 0d6bfb8abbd14b05798b7de307af8c59f47d6425 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 1 Oct 1999 13:44:39 +0000
Subject: deep_gp pour l'écriture dans un fichier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@91 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/pp_control.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 3eb10e6dde..34ebf76fc5 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -76,7 +76,7 @@ let with_output_to ch =
   let ft = with_fp { fp_output = ch ;
       	             fp_output_function = (output ch) ;
 	             fp_flush_function = (fun () -> flush ch) } in
-  set_dflt_gp ft; 
+  set_gp ft deep_gp; 
   ft
 
 let std_ft = Format.std_formatter
-- 
cgit v1.2.3