]> matita.cs.unibo.it Git - helm.git/commitdiff
- bugfix: shows all log while doing 'update'
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 19:53:26 +0000 (19:53 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 26 Dec 2002 19:53:26 +0000 (19:53 +0000)
helm/http_getter/http_getter.ml

index c5d4f169dc672af4a306b4d7d2b084992e92f8e2..0644fcc7d11000003aa8808c770cdebc1bf083ee 100644 (file)
@@ -239,7 +239,7 @@ let update_from_server logmsg server_url = (* use global maps *)
         Pcre.replace ~pat:"^helm:rdf.*//theory:" ~templ:server_url uri
     | uri -> raise (Http_getter_invalid_URI uri)
   in
-  let log = ref ("Processing server: " ^ server_url ^ "<br />\n") in
+  let log = ref (logmsg ^ "Processing server: " ^ server_url ^ "<br />\n") in
   let (xml_index, rdf_index, xsl_index) =
     (* TODO keeps index in memory, is better to keep them on temp files? *)
     (http_get (server_url ^ "/" ^ Http_getter_env.xml_index),