]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite2/grafiteMisc.mli
1. metadata are no longer stored in .moo files.
[helm.git] / helm / ocaml / grafite2 / grafiteMisc.mli
index 8cc384abcd0d38abf3d40691d024cda17f9ae823..9f1486b0b3ce8cedfe616c5e5f8442ed1ee7fbb9 100644 (file)
@@ -33,3 +33,4 @@ val is_empty: string -> bool
 val baseuri_of_file : string -> string
 
 val obj_file_of_script : basedir:string -> string -> string
+val metadata_file_of_script : basedir:string -> string -> string