From 0ac24004d04d605b76932e1f6e84d4e4c0839cb3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 29 Oct 2019 15:24:07 +0100
Subject: [PATCH] [Kernel] Fixes the help message of the deprecated option
-warn-decimal-float.
---
src/kernel_services/plugin_entry_points/kernel.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 3bcff739e6a..651e7f1630b 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"
--
GitLab