From 09c14db5b8930390bfc394857ae0247fb00f139c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Jan 2010 17:34:30 +0000 Subject: [PATCH] Source language path must be appended, not replaced. --- helm/software/matita/matitaGui.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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" -- 2.39.2