]> matita.cs.unibo.it Git - helm.git/commitdiff
added newline to log when log_file is in use
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 16 Apr 2004 12:16:08 +0000 (12:16 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 16 Apr 2004 12:16:08 +0000 (12:16 +0000)
helm/ocaml/getter/http_getter_logger.ml

index c639f6c9087e1805ae99c1aaac7d2a0917552f4f..f77b5eba86613f30b3c09c1b65fe9a0bccfef617 100644 (file)
@@ -55,6 +55,7 @@ let log ?(level = 1) s =
     | None, _ -> prerr_endline msg
     | Some fname, Some oc ->
         output_string oc msg;
+        output_string oc "\n";
         flush oc
     | Some _, None -> assert false