]> matita.cs.unibo.it Git - helm.git/commitdiff
is_empty_listing fixed: the ls method normalizes away the .gz suffix
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Jul 2006 09:54:03 +0000 (09:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 19 Jul 2006 09:54:03 +0000 (09:54 +0000)
components/getter/http_getter_storage.ml

index 23f479c24cd4408de5007e96a536efd37c72b30a..77bfe138da3450d9a484fdf2a6e8681b591d7e83 100644 (file)
@@ -83,7 +83,7 @@ let is_empty_listing files =
   List.for_all
    (fun s ->
      let len = String.length s in
-      len < 7 || String.sub s (len - 7) 7 <> ".xml.gz") files
+      len < 4 || String.sub s (len - 4) 4 <> ".xml") files
 
 (************************* GLOBALS PREFIXES **********************************)