From 736f1c5caccbf659359853b9b0ad426f694c10ae Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 4 Mar 2013 21:50:22 +0100 Subject: [PATCH] Remove dead code. --- src/utils/pretty.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml index abcb59c..a7434b1 100644 --- a/src/utils/pretty.ml +++ b/src/utils/pretty.ml @@ -110,12 +110,6 @@ let overline s = combine_all combining_overbar s let underline s = combine_all combining_underbar s 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 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 i = String.make i ' ' let line i = String.make i '_' -- 2.17.1