projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Simply use String.make for Pretty.padding and Pretty.line, since it's
[tatoo.git]
/
src
/
utils
/
pretty.ml
diff --git
a/src/utils/pretty.ml
b/src/utils/pretty.ml
index
c54d0ed
..
abcb59c
100644
(file)
--- a/
src/utils/pretty.ml
+++ b/
src/utils/pretty.ml
@@
-14,7
+14,7
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-0
1-30 19:08:11
CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-0
3-04 18:46:09
CET by Kim Nguyen>
*)
open Format
*)
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 mk_repeater c =
let mk_str i = String.make i c in
- let _table = Array.init
1
6 mk_str in
+ let _table = Array.init
25
6 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
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
'_'