From: Claudio Sacerdoti Coen Date: Fri, 8 Jan 2010 17:34:30 +0000 (+0000) Subject: Source language path must be appended, not replaced. X-Git-Tag: make_still_working~3134 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09c14db5b8930390bfc394857ae0247fb00f139c;p=helm.git Source language path must be appended, not replaced. --- diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 9459c86ca..deef158a3 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -889,7 +889,9 @@ class gui () = let _ = let source_language_manager = GSourceView2.source_language_manager ~default:true in - source_language_manager#set_search_path[BuildTimeConf.runtime_base_dir]; + source_language_manager#set_search_path + (BuildTimeConf.runtime_base_dir :: + source_language_manager#search_path); match source_language_manager#language "grafite" with | None -> HLog.warn(sprintf "can't load a language file for \"grafite\" in %s"