From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 Oct 2006 14:17:06 +0000 (+0000)
Subject: Better label for the disambiguation errors window.
X-Git-Tag: make_still_working~6700
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=213cac2ec31720d1988c990a4c4ef04d47bb2ff9;p=helm.git

Better label for the disambiguation errors window.
---

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