]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite2/grafiteMisc.ml
1. metadata are no longer stored in .moo files.
[helm.git] / helm / ocaml / grafite2 / grafiteMisc.ml
index 910f8a483dd16617c9e4cfdde5ff8c1b8507f970..8739b7a070fb4c70c2a0b997432684c04197fe6f 100644 (file)
@@ -72,3 +72,8 @@ let baseuri_of_file file =
 let obj_file_of_script ~basedir f =
   let baseuri = baseuri_of_file f in
    LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
+
+let metadata_file_of_script ~basedir f =
+  let baseuri = baseuri_of_file f in
+   LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri
+