From b6856f3de223e50ebeb3c26fd098ab128a5d661f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Dec 2002 19:53:26 +0000 Subject: [PATCH] - bugfix: shows all log while doing 'update' --- helm/http_getter/http_getter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index c5d4f169d..0644fcc7d 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -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 ^ "
\n") in + let log = ref (logmsg ^ "Processing server: " ^ server_url ^ "
\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), -- 2.39.2