diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 6e898e102873e5d7050a32f0b0eae1c176fdb816..da63179bf0fa0632cd2a51a10eafeff0dc914419 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -430,7 +430,7 @@ let run_list_all_plugin_options () = let () = Cmdline.run_after_exiting_stage run_list_all_plugin_options let () = Parameter_customize.set_group help -let () = Parameter_customize.set_cmdline_stage Cmdline.Exiting +let () = Parameter_customize.set_cmdline_stage Cmdline.Extending let () = Parameter_customize.do_not_journalize () let () = Parameter_customize.set_negative_option_name "" module Explain =