Bug fixed: LICENSE and AUTHORS were searched in the current dir :-(

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 3e8fde7a9fc03d3586c7fa6413bde7ff52828408..8dc0cf3135a56b0e4a85e0984d6ad9ef8cc799c3 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -154,7 +154,7 @@ class gui () =
         [ ];
         (* about win *)
       let parse_txt_file file =
-       let ch = open_in file in
+       let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
        let l_rev = ref [] in
        try
         while true do