]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_env.mli
removed dump_env in favour of env_to_string which return a string
[helm.git] / helm / http_getter / http_getter_env.mli
index eab0e79d2b7d37abeb9388568d6a741a46325b1b..41028389de47d4a3e0320839e2c8028628ee58dc 100644 (file)
@@ -60,7 +60,8 @@ val conf_dir      : string          (* directory where conf_file resides *)
 
   (* misc *)
 
-val reload: unit -> unit          (* reload servers list *)
-val dump_env : unit -> unit       (* dump a textual representation of the
-                                  current http_getter settings *)
+val reload: unit -> unit            (* reload servers list *)
+val env_to_string : unit -> string  (* dump a textual representation of the
+                                    current http_getter settings on an output
+                                    channel*)