]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: LICENSE and AUTHORS were searched in the current dir :-(
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 16:37:34 +0000 (16:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Jul 2005 16:37:34 +0000 (16:37 +0000)
helm/matita/matitaGui.ml

index 3e8fde7a9fc03d3586c7fa6413bde7ff52828408..8dc0cf3135a56b0e4a85e0984d6ad9ef8cc799c3 100644 (file)
@@ -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