- added maps sync

[helm.git] / helm / http_getter / http_getter.ml

diff --git a/helm/http_getter/http_getter.ml b/helm/http_getter/http_getter.ml
index c46a793268911ea98ab702dc7dfb48ef159f3691..c5d4f169dc672af4a306b4d7d2b084992e92f8e2 100644 (file)
--- a/helm/http_getter/http_getter.ml
+++ b/helm/http_getter/http_getter.ml
@@ -328,9 +328,7 @@ 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;
+        (xml_map#clear; rdf_map#clear; xsl_map#clear;
         let log =
           List.fold_left
             update_from_server
@@ -338,6 +336,7 @@ let callback (req: Http_types.request) outchan =
               (* reverse order: 1st server is the most important one *)
             (List.rev Http_getter_env.servers)
         in
+        xml_map#sync; rdf_map#sync; xsl_map#sync;
         return_html_msg log outchan)
     | "/getalluris" ->
         return_all_xml_uris