]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/getter/http_getter_md5.ml
New argument (the identifier) to generalize.
[helm.git] / helm / ocaml / getter / http_getter_md5.ml
1 (* md5 helpers *)
2 let md5_create files reg =
3   let opts = "md5sum " ^ String.concat " " files ^ " > " ^ reg in
4   let rc = Unix.system opts in
5   match rc with
6   | Unix.WEXITED 0 -> ()
7   | Unix.WEXITED i -> raise (Failure "Unable to create the md5sums file")
8   | _ -> assert false 
9
10 let md5_check reg = 
11   let opts = "md5sum -c " ^ reg in
12   let rc = Unix.system opts in
13   match rc with
14   | Unix.WEXITED 0 -> true
15   | Unix.WEXITED _ -> false 
16   | _ -> assert false 
17
18 let reg () = (Lazy.force Http_getter_env.dump_file) ^ ".md5"
19
20 (* sync checks *)
21
22 (* maybe should be useda as a fallback *)
23 (*
24 let is_in_sync_date () =
25   let get_last_mod_date f =
26     try 
27       (Unix.stat f).Unix.st_mtime
28     with 
29     | Unix.Unix_error (Unix.ENOENT, _, _)-> 0.0 
30   in
31   let map_date = get_last_mod_date (Lazy.force Http_getter_env.cic_dbm_real) in
32   let dump_date = get_last_mod_date (Lazy.force Http_getter_env.dump_file) in
33   dump_date < map_date
34 *)
35
36 let check_hash () =
37   md5_check (reg ())
38
39 let create_hash files = 
40   md5_create files (reg ())
41
42