X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=f849dc25f5b5e84d09e067dd759687da415a0918;hb=69a723299ea4c9ba4087a87e60c6fbeef4c1d33d;hp=5bab5ab0ab4dcad44763fca84578cbe89c966ea8;hpb=b74ef6550e31214a340dfeae67ce77d055e9827c;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5bab5ab0a..f849dc25f 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1379,11 +1379,13 @@ class gui () = end method setStar name b = - let l = main#scriptLabel in + let w = main#toplevel in + let set x = w#set_title x in + let name = "Matita - " ^ name in if b then - l#set_text (name ^ " *") + set (name ^ " *") else - l#set_text (name) + set (name) method private _enableSaveTo file = script_fname <- Some file;