diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 5ffc6d21ff0617a4ecadfcfa33c04d5b13f51e80..88e6d32d72ecbf5d8912c5d5d18d6c1a0f80b71f 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -1867,14 +1867,7 @@ module CacheSize = let () = CacheSize.set_range ~min:1 ~max:10 let () = CacheSize.add_update_hook (fun _ i -> Binary_cache.set_cache_size i) -(* ************************************************************************* *) -(** {2 Other options} *) -(* ************************************************************************* *) - -[@@@warning "-60"] -(* Warning: these options are parsed and used directly from Cmdline *) - -let () = Parameter_customize.set_group project +let () = Parameter_customize.set_group performance let () = Parameter_customize.set_negative_option_name "" let () = Parameter_customize.set_cmdline_stage Cmdline.Early module Deterministic = @@ -1886,6 +1879,10 @@ module Deterministic = let help = "" end) +(* ************************************************************************* *) +(** {2 Other options} *) +(* ************************************************************************* *) + let () = Parameter_customize.set_group checks let () = Parameter_customize.do_not_projectify () let () = Parameter_customize.set_negative_option_name "" @@ -1899,8 +1896,6 @@ module Permissive = "perform less verifications on validity of command-line options" end) -[@@@warning "+60"] - (* Local Variables: compile-command: "make -C ../../.."