diff options
Diffstat (limited to 'ide/utils/configwin_types.ml')
| -rw-r--r-- | ide/utils/configwin_types.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml index bf2b74ee63..90d5756b8f 100644 --- a/ide/utils/configwin_types.ml +++ b/ide/utils/configwin_types.ml @@ -244,10 +244,6 @@ type modifiers_param = { } -let mk_custom_text_string_param (a : 'a string_param) : string string_param = - Obj.magic a - - (** This type represents the different kinds of parameters. *) type parameter_kind = String_param of string string_param |