From b47bd5617018145332deaa75e42ddad0728d9638 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 23 Feb 2017 13:34:17 +0100
Subject: [safe-string] lib/miscelanea

No functional change.js
---
 lib/pp_control.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/pp_control.ml')

diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 890ffe0a18..ab8dc0798c 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -58,7 +58,7 @@ let with_fp chan out_function flush_function =
 (* Output on a channel ch *)
 
 let with_output_to ch =
-  let ft = with_fp ch (output ch) (fun () -> flush ch) in
+  let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in
   set_gp ft deep_gp;
   ft
 
-- 
cgit v1.2.3