diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml index 191cd1db47fe5e961eae8542209a3742b0595a1b..5321356107d0fff8f117901029b7cff6bb6f0ef3 100644 --- a/src/kernel_services/plugin_entry_points/plugin.ml +++ b/src/kernel_services/plugin_entry_points/plugin.ml @@ -295,6 +295,11 @@ struct let is_visible = !share_visible_ref let is_kernel = is_kernel () (* the side effect must be applied right now *) + let () = + Parameter_customize.set_cmdline_stage Cmdline.Extended; + if is_visible then Parameter_customize.is_reconfigurable () + else Parameter_customize.is_invisible () + module Dir_name = Filepath (struct