]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/getter/http_getter_storage.ml
is_top_down was not propageted correctly under a bottom-up conversion.
[helm.git] / helm / software / components / getter / http_getter_storage.ml
index 3650d79b95f0bc9b492271a4ea35db4d64e150eb..77bfe138da3450d9a484fdf2a6e8681b591d7e83 100644 (file)
@@ -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 < 4 || String.sub s (len - 4) 4 <> ".xml") files
 
 (************************* GLOBALS PREFIXES **********************************)
     
@@ -295,7 +298,10 @@ let exists s =
   with Resource_not_found _ -> false
 
 let resolve ?(must_exists=true) ~writable =
-  dispatch_single 
+  (if must_exists then
+    dispatch_multi
+  else
+    dispatch_single)
     { write = writable;
       name="resolve"; 
       exists = must_exists;