X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgetter%2Fhttp_getter_storage.mli;h=cc0ff46c4797ee77c76fc9005937bb0880498796;hb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;hp=04af29f0ce4a2929cb8837d4ee018e74cecc7d49;hpb=2ce7fd1b8d48f86d1f93231fe35473551cd060e7;p=helm.git diff --git a/helm/software/components/getter/http_getter_storage.mli b/helm/software/components/getter/http_getter_storage.mli index 04af29f0c..cc0ff46c4 100644 --- a/helm/software/components/getter/http_getter_storage.mli +++ b/helm/software/components/getter/http_getter_storage.mli @@ -43,7 +43,7 @@ exception Resource_not_found of string * string (** method, uri *) (** @return a list of string where dir are returned with a trailing "/" *) -val ls: string -> string list +val ls: local:bool -> string -> string list (** @return the filename of the resource corresponding to a given uri. Handle @@ -53,20 +53,21 @@ val ls: string -> string list * that the search is performed only if the asked resource is not found in * cache (i.e. to perform the find again you need to clean the cache). * Defaults to false *) -val filename: ?find:bool -> string -> string +val filename: local:bool -> ?find:bool -> string -> string (** only works for local resources * if both compressed and non-compressed versions of a resource exist, both of * them are removed *) val remove: string -> unit -val exists: string -> bool -val resolve: ?must_exists:bool -> writable:bool -> string -> string +val exists: local:bool -> string -> bool +val resolve: + local:bool -> ?must_exists:bool -> writable:bool -> string -> string (* val get_attrs: string -> Http_getter_types.prefix_attr list *) val is_read_only: string -> bool val is_legacy: string -> bool -val is_empty: string -> bool +val is_empty: local:bool -> string -> bool val clean_cache: unit -> unit