From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 13 Dec 2005 14:42:57 +0000 (+0000)
Subject: added ensure_path_exists to save_moo
X-Git-Tag: make_still_working~8003
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d4a3a25b327bb2c15bd0cff116ba6698b1a4335;p=helm.git

added ensure_path_exists to save_moo
---

diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml
index 8c6928b7b..bf02e91ac 100644
--- a/helm/ocaml/grafite/grafiteMarshal.ml
+++ b/helm/ocaml/grafite/grafiteMarshal.ml
@@ -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