From 213cac2ec31720d1988c990a4c4ef04d47bb2ff9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Oct 2006 14:17:06 +0000 Subject: [PATCH] Better label for the disambiguation errors window. --- helm/software/matita/matitaGui.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index aaacc178e..998cdc339 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -310,7 +310,7 @@ let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn let model = new interpErrorModel dialog#treeview choices in dialog#disambiguationErrors#set_title "Disambiguation error"; dialog#disambiguationErrorsLabel#set_label - "Click on an interpretation to see the corresponding error message:"; + "Click on an error to see the corresponding message:"; ignore (dialog#treeview#connect#cursor_changed (fun _ -> let tree_path = match fst (dialog#treeview#get_cursor ()) with -- 2.39.2