diff options
Diffstat (limited to 'driver/main_args.mli')
| -rw-r--r-- | driver/main_args.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/main_args.mli b/driver/main_args.mli index f39482d21f..38654b694d 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -136,6 +136,7 @@ module type Optcommon_options = sig val _inline_indirect_cost : string -> unit val _inline_lifting_benefit : string -> unit val _unbox_closures : unit -> unit + val _unbox_closures_factor : int -> unit val _inline_branch_factor : string -> unit val _remove_unused_arguments : unit -> unit val _no_unbox_free_vars_of_closures : unit -> unit |