From 1f252a3fe87fa261028d026235be17ef02596c97 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 12 Nov 2007 21:14:49 +0000
Subject: [PATCH] since there is no more tab, the modification of the current
 file is in the window title

---
 matita/matitaGui.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 5bab5ab0a..f849dc25f 100644
--- a/matita/matitaGui.ml
+++ b/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;
-- 
2.39.2