From: Stefano Zacchiroli Date: Fri, 23 Dec 2005 10:43:14 +0000 (+0000) Subject: minor fixes (-nodb works again) X-Git-Tag: make_still_working~7921 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=114ee592d3da9b49abfd4c1b186cba1e170075dc;p=helm.git minor fixes (-nodb works again) --- diff --git a/helm/ocaml/lexicon/lexiconEngine.ml b/helm/ocaml/lexicon/lexiconEngine.ml index ff186b131..752dabb71 100644 --- a/helm/ocaml/lexicon/lexiconEngine.ml +++ b/helm/ocaml/lexicon/lexiconEngine.ml @@ -108,7 +108,7 @@ let rec eval_command status cmd = let lexicon = LexiconMarshal.load_lexicon lexiconpath in let status = List.fold_left eval_command status lexicon in if Helm_registry.get_bool "db.nodb" then - let metadatapath = baseuri ^ ".metadata" in + let metadatapath = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in if not (Sys.file_exists metadatapath) then raise (MetadataNotFound metadatapath) else diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml index 5da9507fc..092527155 100644 --- a/helm/ocaml/library/libraryClean.ml +++ b/helm/ocaml/library/libraryClean.ml @@ -147,15 +147,15 @@ let moo_root_dir = lazy ( let close_nodb ~basedir buris = let rev_deps = Hashtbl.create 97 in - let all_moos = - HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo") + let all_metadata = + HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata") (Lazy.force moo_root_dir) in List.iter (fun path -> let metadata = LibraryNoDb.load_metadata ~fname:path in - let baseuri_of_current_moo = - let dirname = Filename.chop_extension (Filename.dirname path) in + let baseuri_of_current_metadata = + let dirname = Filename.dirname path in let basedirlen = String.length basedir in assert (String.sub dirname 0 basedirlen = basedir); "cic:" ^ @@ -168,8 +168,8 @@ let close_nodb ~basedir buris = metadata in List.iter - (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps) - all_moos; + (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps) + all_metadata; let buris_to_remove = HExtlib.list_uniq (List.fast_sort Pervasives.compare