From f4117d09d2bdba02657ed83ab98cfae8c90cf8d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jul 2008 10:54:28 +0000 Subject: [PATCH] better tex/utf8 win --- helm/software/matita/matitaGui.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5d9d87c86..c1f9a992a 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -913,10 +913,10 @@ class gui () = connect_menu_item main#showUnicodeTable (fun _ -> let text = String.concat "\n" - (List.map (fun (k,vs) -> "\t" ^ k ^ "\t" ^ String.concat ", " vs) + (List.map (fun (k,vs) -> k ^ "\t" ^ String.concat ", " vs) (Utf8Macro.pp_table ())) in - let w = MatitaGtkMisc.new_search_win "Tex/UTF8 table" text in + let w = MatitaGtkMisc.new_search_win "TeX/UTF8 table" text in w#toplevel#set_transient_for (main#toplevel#as_window); w#toplevel#show ()); (* script monospace font stuff *) -- 2.39.2