- let moo_fname = MatitacleanLib.obj_file_of_script fname in
- MatitaMoo.save_moo moo_fname moo_content_rev;
- MatitaLog.message
+ let basedir = Helm_registry.get "matita.basedir" in
+ let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+ GrafiteMarshal.save_moo moo_fname moo_content_rev;
+ LibraryNoDb.save_metadata metadata_fname metadata;
+ HLog.message