From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Jul 2006 13:57:43 +0000 (+0000)
Subject: Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon... 
X-Git-Tag: make_still_working~7052
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9052c3d19ade20c086bb114133fe7cd060e23ec4;p=helm.git

Quick&dirty patch to make Http_getter_storage.is_empty ignore {.moo,.metadata.lexicon} files.
---

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 **********************************)