]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarian.ml
better doc and root/depends file parsing
[helm.git] / components / library / librarian.ml
index 9a16e814d56527354b66d4e8d5d5bdc6477795a3..f2268488f2afbc3ce975578c072a172af1ec72ac 100644 (file)
@@ -38,10 +38,11 @@ let remove_trailing_slash s =
 let load_root_file rootpath =
   let data = HExtlib.input_file rootpath in
   let lines = Str.split (Str.regexp "\n") data in
+  let clean s = Pcre.replace ~pat:"^ *" (Pcre.replace ~pat:" *$" s) in
   List.map 
     (fun l -> 
       match Str.split (Str.regexp "=") l with
-      | [k;v] -> Pcre.replace ~pat:"^ *" k, Pcre.replace ~pat:" *$" v
+      | [k;v] -> clean k, Http_getter_misc.strip_trailing_slash (clean v)
       | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
     lines
 ;;