let basedir = Helm_registry.get "matita.basedir" in
let save () =
let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
- GrafiteMarshal.save_moo moo_fname
- status.GrafiteTypes.moo_content_rev in
+ let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+ GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
+ LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+ in
if (MatitaScript.current ())#eos &&
status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
then