Dune sites used to locate the standard library

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

diff --git a/matita/matita/buildTimeConf.ml b/matita/matita/buildTimeConf.ml
index fab7db0cdb97d4ae6f61fa827f6338962835c6b6..3774aaf35a9087358926efa5da731ec4c43d4a99 100644 (file)
--- a/matita/matita/buildTimeConf.ml
+++ b/matita/matita/buildTimeConf.ml
@@ -40,7 +40,10 @@ let script_font = "Monospace";;
 let runtime_base_dir =
   try
     Sys.getenv "MATITA_RT_BASE_DIR"
-  with Not_found -> "/home/claudio/ricerca/matita5/helm/matita/matita";;
+  with Not_found ->
+   match Mysites.Sites.myshare with
+      [rt] -> rt (*It was: "/home/claudio/ricerca/matita5/helm/matita/matita"*)
+    | _ -> assert false
 
 let images_dir = runtime_base_dir ^ "/icons"
 let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc"