From 4e683370099ea7aaea877bc345ca8821938d49ed Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 7 Jan 2003 18:23:24 +0000 Subject: [PATCH] - reload servers list on before /update --- helm/http_getter/http_getter.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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) -- 2.39.2