diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 3bcff739e6a5064f21a7fd18923c3992c43c6ce3..651e7f1630b5c3fd3aea7c6e1823ea8bc47876c9 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -996,8 +996,8 @@ module WarnDecimalFloat = String(struct let option_name = "-warn-decimal-float" let arg_name = "freq" - let help = "[DEPRECATED: Use -kernel-warn-key decimal-float \ - (and similar options) instead] \ + let help = "[DEPRECATED: Use -kernel-warn-key \ + parser:decimal-float=active (or inactive) instead] \ Warn when floating-point constants cannot be exactly \ represented; freq must be one of none, once or all" let default = "once"