From: Andrea Asperti Date: Wed, 13 Oct 2004 07:18:40 +0000 (+0000) Subject: get_and_save now handles big files properly (i.e. doesn't hold them X-Git-Tag: V_0_0_10~84 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ba7f920fa28fd31f9eaf33b1511bec6aee268eba;p=helm.git get_and_save now handles big files properly (i.e. doesn't hold them entirely in memory) --- diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index 9b4237811..295c638b9 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -14,10 +14,10 @@ http_getter_env.cmo: http_getter_const.cmi http_getter_logger.cmi \ http_getter_misc.cmi http_getter_types.cmo http_getter_env.cmi http_getter_env.cmx: http_getter_const.cmx http_getter_logger.cmx \ http_getter_misc.cmx http_getter_types.cmx http_getter_env.cmi -http_getter_common.cmo: http_getter_env.cmi http_getter_logger.cmi \ - http_getter_misc.cmi http_getter_types.cmo http_getter_common.cmi -http_getter_common.cmx: http_getter_env.cmx http_getter_logger.cmx \ - http_getter_misc.cmx http_getter_types.cmx http_getter_common.cmi +http_getter_common.cmo: http_getter_env.cmi http_getter_misc.cmi \ + http_getter_types.cmo http_getter_common.cmi +http_getter_common.cmx: http_getter_env.cmx http_getter_misc.cmx \ + http_getter_types.cmx http_getter_common.cmi http_getter_map.cmo: http_getter_map.cmi http_getter_map.cmx: http_getter_map.cmi http_getter_cache.cmo: http_getter_common.cmi http_getter_env.cmi \ diff --git a/helm/ocaml/getter/clientHTTP.ml b/helm/ocaml/getter/clientHTTP.ml index 12641147f..b4e0e26b6 100644 --- a/helm/ocaml/getter/clientHTTP.ml +++ b/helm/ocaml/getter/clientHTTP.ml @@ -40,10 +40,9 @@ let get uri = ;; let get_and_save uri dest_filename = - let reply = get uri - and out_channel = open_out dest_filename in - output_string out_channel reply ; - close_out out_channel + let out_channel = open_out dest_filename in + Http_user_agent.get_iter (output_string out_channel) uri; + close_out out_channel ;; let get_and_save_to_tmp uri =