now baseuri is needed in each file (and its redefinition is forbidden)

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 95de73528cf8ba1b273002e395026d11c2935d59..222ca491b9745b80eed476b5274b62f3941d2e08 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -585,16 +585,18 @@ let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 
 let default_options () =
+(*
   let options =
     StringMap.add "baseuri"
       (String
         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
       no_options
   in
+*)
   let options =
     StringMap.add "basedir"
       (String (Helm_registry.get "matita.basedir" ))
-      options
+      no_options
   in
   options