From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 16 Apr 2004 12:16:08 +0000 (+0000)
Subject: added newline to log when log_file is in use
X-Git-Tag: dead_dir_walking~54
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eed9cd448726bb9db34ac69e8e137460e691bcfc;p=helm.git

added newline to log when log_file is in use
---

diff --git a/helm/ocaml/getter/http_getter_logger.ml b/helm/ocaml/getter/http_getter_logger.ml
index c639f6c90..f77b5eba8 100644
--- a/helm/ocaml/getter/http_getter_logger.ml
+++ b/helm/ocaml/getter/http_getter_logger.ml
@@ -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