]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/http_getter.ml
A lazy value was put in place of a function ==> the memoized value was no
[helm.git] / helm / ocaml / getter / http_getter.ml
index 38683430d106c99d5da66d2d3fd2e23327c99cf0..21ed483ad157bc64de0abe11bdf4b100766d3908 100644 (file)
@@ -164,7 +164,7 @@ let update_from_all_servers () =  (* use global maps *)
       update_from_server
       []  (* initial logmsg: empty *)
         (* reverse order: 1st server is the most important one *)
-      (List.map snd (List.rev (Lazy.force Http_getter_env.servers)))
+      (List.map snd (List.rev (Http_getter_env.servers ())))
   in
   sync_maps ();
   `Msg (`L (List.rev log))
@@ -309,7 +309,7 @@ let list_servers () =
   if remote () then
     list_servers_remote ()
   else
-    Lazy.force Http_getter_env.servers
+    Http_getter_env.servers ()
 
 let add_server ?(position = 0) name =
   if remote () then
@@ -331,7 +331,7 @@ let remove_server position =
   else begin
     let server_name =
       try
-        List.assoc position (Lazy.force Http_getter_env.servers)
+        List.assoc position (Http_getter_env.servers ())
       with Not_found ->
         raise (Invalid_argument (sprintf "no server with position %d" position))
     in