]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_misc.mli
- moved wget, gzip, gunzip, tempfile from Http_getter_common to
[helm.git] / helm / http_getter / http_getter_misc.mli
index c1afb198ff8f704a88facc780cb2d5a7696210ac..bb99827de0ebd15e66f8ef2bbcbecbd88e42ddf0 100644 (file)
@@ -31,3 +31,10 @@ val iter_file : (string -> unit) -> string -> unit
 val hashtbl_sorted_fold :
   ('a -> 'b -> 'c -> 'c) -> ('a, 'b) Hashtbl.t -> 'c -> 'c
 
+val wget: ?output: string -> string -> unit
+val gzip: ?keep: bool -> string -> unit
+val gunzip: ?keep: bool -> string -> unit
+val tempfile: unit -> string
+
+val string_of_proc_status : Unix.process_status -> string
+