From d16314f40989a63bbd1119a9701fa44e336599ff Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kn@lri.fr>
Date: Mon, 4 Mar 2013 18:53:38 +0100
Subject: [PATCH] Simply use String.make for Pretty.padding and Pretty.line,
 since it's only used in places where performance is not critical.

---
 src/utils/pretty.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml
index c54d0ed..abcb59c 100644
--- a/src/utils/pretty.ml
+++ b/src/utils/pretty.ml
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-01-30 19:08:11 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-03-04 18:46:09 CET by Kim Nguyen>
 *)
 
 open Format
@@ -112,12 +112,12 @@ let strike s = combine_all combining_stroke s
 
 let mk_repeater c =
   let mk_str i = String.make i c in
-  let _table = Array.init 16 mk_str in
+  let _table = Array.init 256 mk_str in
      fun i -> try
       if i < 16 then _table.(i) else mk_str i
     with e -> print_int i; print_newline(); raise e
-let padding = mk_repeater ' '
-let line = mk_repeater '_'
+let padding i = String.make i ' '
+let line i = String.make i '_'
 
 
 
-- 
2.17.1