From: Ferruccio Guidi Date: Sat, 25 Jun 2011 19:26:02 +0000 (+0000) Subject: long file names caused indentation underflow (String.make) when times X-Git-Tag: make_still_working~2391 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e8ff5ae44f5dc285f5180543db6a6745ffad7a82;p=helm.git long file names caused indentation underflow (String.make) when times were displayed --- diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 01f070e2b..144250fb9 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -78,8 +78,8 @@ let print_string = match right_justify with None -> "" | Some (ss,len_ss) -> - assert (80 - !indent - len_ss - String.length s >= 0); - String.make (80 - !indent - len_ss - String.length s) ' ' ^ ss + let i = 80 - !indent - len_ss - String.length s in + if i > 0 then String.make i ' ' ^ ss else ss in assert (!indent >=0); print_string (String.make !indent ' ' ^ s ^ ss) in