From 9052c3d19ade20c086bb114133fe7cd060e23ec4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Jul 2006 13:57:43 +0000 Subject: [PATCH] Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files. --- helm/software/components/getter/http_getter_storage.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/getter/http_getter_storage.ml b/helm/software/components/getter/http_getter_storage.ml index b1a05d996..23f479c24 100644 --- a/helm/software/components/getter/http_getter_storage.ml +++ b/helm/software/components/getter/http_getter_storage.ml @@ -80,7 +80,10 @@ let is_file_schema url = Pcre.pmatch ~rex:file_scheme_RE url let is_http_schema url = Pcre.pmatch ~rex:http_scheme_RE url let is_empty_listing files = - List.for_all (fun s -> s.[String.length s - 1] = '/') files + List.for_all + (fun s -> + let len = String.length s in + len < 7 || String.sub s (len - 7) 7 <> ".xml.gz") files (************************* GLOBALS PREFIXES **********************************) -- 2.39.2