]> matita.cs.unibo.it Git - helm.git/commitdiff
According to the Gnome Interface Guidelines the Help menu must be aliged
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 16:18:10 +0000 (16:18 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Jul 2005 16:18:10 +0000 (16:18 +0000)
as the other ones. It should not be all alone on the very right of the screen.

helm/matita/matitaGui.ml

index 90826e98f9f6e72265313c65495798849b5913a3..0a0239aeb4769b7eaff04b8a84c4ba8c265bb74b 100644 (file)
@@ -487,7 +487,6 @@ class gui () =
         | `DELETE_EVENT -> return None));
         (* menus *)
       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
-      main#helpMenu#set_right_justified true;
         (* console *)
       let adj = main#logScrolledWin#vadjustment in
         ignore (adj#connect#changed