X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibraryMisc.ml;h=7c82e27c40f3dd9564674e6d8c7c3c1a2ffb13d8;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=e971c52d4b09cfe489ac27facb5e0c43729de748;hpb=4e238c92f66aedf21c2d3a33aa5215cdf0a7189f;p=helm.git diff --git a/helm/software/components/library/libraryMisc.ml b/helm/software/components/library/libraryMisc.ml index e971c52d4..7c82e27c4 100644 --- a/helm/software/components/library/libraryMisc.ml +++ b/helm/software/components/library/libraryMisc.ml @@ -25,16 +25,14 @@ (* $Id$ *) -let resolve ~must_exist ~writable baseuri = +let resolve ~must_exist ~writable ~local baseuri = if must_exist then - Http_getter.resolve ~writable baseuri + Http_getter.resolve ~local ~writable baseuri else - Http_getter.filename ~writable baseuri + Http_getter.filename ~local ~writable baseuri let obj_file_of_baseuri ~must_exist ~writable ~baseuri = - resolve ~must_exist ~writable baseuri ^ ".moo" + resolve ~must_exist ~writable ~local:true baseuri ^ ".moo" let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri = - resolve ~must_exist ~writable baseuri ^ ".lexicon" -let metadata_file_of_baseuri~must_exist ~writable ~baseuri = - resolve ~must_exist ~writable baseuri ^ ".metadata" + resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon"