From 2b1141b5a01288a1d6a3fd54e5bb2763ed905718 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Wed, 3 Jul 2019 17:59:14 +0200 Subject: [PATCH] [Kernel] Makes the -explain option independent of -then. --- src/kernel_services/plugin_entry_points/kernel.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 6e898e10287..da63179bf0f 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 = -- GitLab