]> matita.cs.unibo.it Git - helm.git/commitdiff
fix
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 14 Jun 2005 11:54:31 +0000 (11:54 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 14 Jun 2005 11:54:31 +0000 (11:54 +0000)
helm/graphs/tools/drawGraph.ml

index 9f86feeb074de7700501acc7196f168d5b7fc276..c17902fbc551dd85e92f0a4a5315fee500d978f7 100644 (file)
@@ -35,7 +35,7 @@ let daemon_name = "Draw Graph";;
 let wget url fname =
   prerr_endline (sprintf "DEBUG: wgetting url '%s'" url);
   let oc = open_out fname in
-  Http_client.http_get_iter (output_string oc) url;
+  Http_user_agent.get_iter (output_string oc) url;
   close_out oc
 ;;