]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mmlinterface.ml
Bug fixew
[helm.git] / helm / interface / mmlinterface.ml
index cfccfbb3f18b8b38de75f406b2677f567d7546ff..496e35e55527af64d82782983d18b8a642d0483c 100755 (executable)
@@ -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