From: Stefano Zacchiroli Date: Tue, 7 Jan 2003 18:23:24 +0000 (+0000) Subject: - reload servers list on before /update X-Git-Tag: v0_3_99~75 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4e683370099ea7aaea877bc345ca8821938d49ed - reload servers list on before /update --- diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml index 02877b012..e03817a22 100644 --- a/helm/http_getter/http_getter.ml +++ b/helm/http_getter/http_getter.ml @@ -347,13 +347,14 @@ let callback (req: Http_types.request) outchan = return_html_msg "Register done" outchan | _ -> assert false) | "/update" -> - (xml_map#clear; rdf_map#clear; xsl_map#clear; + (Http_getter_env.reload (); (* reload servers list from servers file *) + xml_map#clear; rdf_map#clear; xsl_map#clear; let log = List.fold_left update_from_server "" (* initial logmsg: empty *) (* reverse order: 1st server is the most important one *) - (List.rev Http_getter_env.servers) + (List.rev !Http_getter_env.servers) in xml_map#sync; rdf_map#sync; xsl_map#sync; return_html_msg log outchan)