]> matita.cs.unibo.it Git - helm.git/commitdiff
* [Luca] string concatenation now made using String.concat instead of
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 May 2004 15:57:23 +0000 (15:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 May 2004 15:57:23 +0000 (15:57 +0000)
  List.fold_left

helm/DEVEL/rdfly/rdfly.ml

index da06477dc652a7e1d8cfe5f4788c7b0f3fab482f..d0bddd8ec21e51e7070ee9eaa27aa45d81523514 100644 (file)
@@ -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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ;