First steps towards a multi-document interface.

[helm.git] / matita / matita / matita.ml

diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml
index 4b8548f1932386d13f024f2f82e5789479b0409b..ee20eda897c22d9f598f5d7cf0f987d1da834fcf 100644 (file)
--- a/matita/matita/matita.ml
+++ b/matita/matita/matita.ml
@@ -59,7 +59,6 @@ let script =
           ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
           () ~id:"boh?" uris
         with MatitaTypes.Cancel -> [])
-      ~set_star:gui#setStar
       ~ask_confirmation:
         (fun ~title ~message -> 
             MatitaGtkMisc.ask_confirmation ~title ~message