diff options
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 32 |
1 files changed, 15 insertions, 17 deletions
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index ff74a3c33..763f99915 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -1282,23 +1282,21 @@ let list ?(editable=true) ?help label (f_strings : 'a -> string list) v = List_param (fun tt -> - Obj.magic - (new list_param_box - { - list_label = label ; - list_help = help ; - list_value = v ; - list_editable = editable ; - list_titles = titles; - list_eq = eq ; - list_strings = f_strings ; - list_color = color ; - list_f_edit = edit ; - list_f_add = add ; - list_f_apply = f ; - } - tt - ) + new list_param_box + { + list_label = label ; + list_help = help ; + list_value = v ; + list_editable = editable ; + list_titles = titles; + list_eq = eq ; + list_strings = f_strings ; + list_color = color ; + list_f_edit = edit ; + list_f_add = add ; + list_f_apply = f ; + } + tt ) (** Create a strings param. *) |