From f1eb1ddb48a3c76b334f992a9902ccbdcd054f8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 17 Jan 2025 15:50:51 +0100
Subject: [PATCH] [Kernel] Moves option "-deterministic" into the new
"performance" group.
---
src/kernel_services/plugin_entry_points/kernel.ml | 15 +++++----------
1 file changed, 5 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 5ffc6d21ff..88e6d32d72 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 ../../.."
--
GitLab