]> matita.cs.unibo.it Git - helm.git/blobdiff - components/lexicon/lexiconEngine.ml
Useless code simplified out.
[helm.git] / components / lexicon / lexiconEngine.ml
index 6e3c1b53d2c5aff600c98ea970689c493dc737e1..d3a8954ff7479be5978ad73d62126d51f8238f28 100644 (file)
@@ -111,8 +111,10 @@ let rec eval_command status cmd =
   match cmd with
   | LexiconAst.Include (loc, baseuri) ->
      let lexiconpath_rw, lexiconpath_r = 
-       LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri,
-       LibraryMisc.lexicon_file_of_baseuri ~writable:false ~baseuri
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~writable:true ~baseuri,
+       LibraryMisc.lexicon_file_of_baseuri 
+         ~must_exist:false ~writable:false ~baseuri
      in
      let lexiconpath = 
        if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
@@ -123,8 +125,10 @@ let rec eval_command status cmd =
      let status = List.fold_left eval_command status lexicon in
       if Helm_registry.get_bool "db.nodb" then
        let metadatapath_rw, metadatapath_r = 
-         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:true,
-         LibraryMisc.metadata_file_of_baseuri ~baseuri ~writable:false
+         LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~baseuri ~writable:true,
+         LibraryMisc.metadata_file_of_baseuri 
+           ~must_exist:false ~baseuri ~writable:false
        in
        let metadatapath =
         if Sys.file_exists metadatapath_rw then metadatapath_rw else