]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mmlinterface.ml
This commit was manufactured by cvs2svn to create tag 'v0_0_2'.
[helm.git] / helm / interface / mmlinterface.ml
index ddb273c894b2c7cf6f1a49672e76d548070b3d65..64c068fc3b55da06d7a70dd1ff28806d6f7bc9e9 100755 (executable)
@@ -683,7 +683,9 @@ object(self)
   ignore(output#connect#selection_changed (choose_selection self)) ;
   ignore(nextb#connect#clicked (next self)) ;
   ignore(prevb#connect#clicked (prev self)) ;
-  ignore(checkb#connect#clicked (check self)) ;
+  (* LUCA: check disabled while compression is not fully implemented *)
+  (* ignore(checkb#connect#clicked (check self)) ; *)
+  checkb#misc#set_sensitive false ;
   ignore(closeb#connect#clicked window#misc#hide) ;
   ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
   let settings_window = new settings_window output scrolled_window0