modifications to make matita behave reasonably, removed some useless windows

[helm.git] / matita / matitaGuiTypes.mli

diff --git a/matita/matitaGuiTypes.mli b/matita/matitaGuiTypes.mli
index 67d431040df41af64635e4f4e501c9e57d9cd114..71cda4ac9d42044e0e2def2d89113fddcba8f740 100644 (file)
--- a/matita/matitaGuiTypes.mli
+++ b/matita/matitaGuiTypes.mli
@@ -93,7 +93,7 @@ object
   method askText: ?title:string -> ?msg:string -> unit -> string option
 
   method loadScript: string -> unit
-  method setStar: string -> bool -> unit
+  method setStar: bool -> unit
 
     (** {3 Fonts} *)
   method increaseFontSize: unit -> unit