]> matita.cs.unibo.it Git - helm.git/commitdiff
added ensure_path_exists to save_moo
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Dec 2005 14:42:57 +0000 (14:42 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Dec 2005 14:42:57 +0000 (14:42 +0000)
helm/ocaml/grafite/grafiteMarshal.ml

index 8c6928b7b6423b41e217c70074bd49322721ffd1..bf02e91ac575604f0934e2d93521c4d7db4045f5 100644 (file)
@@ -69,6 +69,11 @@ let rehash_cmd_uris =
  *)
 
 let save_moo ~fname moo =
+ let ensure_path_exists path =
+   let dir = Filename.dirname path in
+   HExtlib.mkdir dir
+ in
+ ensure_path_exists fname;
  let oc = open_out fname in
  let marshalled = Marshal.to_string (List.rev moo) marshal_flags in
  let checksum = Hashtbl.hash marshalled in