X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=496e35e55527af64d82782983d18b8a642d0483c;hb=21029c2bc06d1467c21763abe36aaaf7b8afd8ca;hp=cfccfbb3f18b8b38de75f406b2677f567d7546ff;hpb=73b8a2b8989ae956eef00d63c2eaaf715428e177;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index cfccfbb3f..496e35e55 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -487,7 +487,7 @@ class settings_window output sw button_export_to_postscript jump_callback let table = GPack.table ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#(pack () in + ~border_width:5 ~packing:vbox#add () in let button_t1 = GButton.toggle_button ~label:"activate t1 fonts" ~packing:(table#attach ~left:0 ~top:0) () in