From: Claudio Sacerdoti Coen Date: Tue, 18 May 2004 15:57:23 +0000 (+0000) Subject: * [Luca] string concatenation now made using String.concat instead of X-Git-Tag: V_0_0_9~44 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b3fdada9a2439c2ce1320350252e330be490b2da * [Luca] string concatenation now made using String.concat instead of List.fold_left --- diff --git a/helm/DEVEL/rdfly/rdfly.ml b/helm/DEVEL/rdfly/rdfly.ml index da06477dc..d0bddd8ec 100644 --- a/helm/DEVEL/rdfly/rdfly.ml +++ b/helm/DEVEL/rdfly/rdfly.ml @@ -24,7 +24,7 @@ let mk_new_msg () = ref [] let msg_output_string msg s = msg := s::!msg let msg_serialize msg = - List.fold_left (fun acc s -> s ^ acc) "" !msg + String.concat "" (List.rev !msg) let msg_output_header msg obj = msg_output_string msg "\n\n" ;