From d2b7fc6f94f26eb8686fe5c0bc73a1c992717854 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 2 Mar 2020 14:02:40 +0100
Subject: [PATCH] [kernel] Reformulate the -warn-special-float help message to
respect the order of possible options.
---
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 e0c3ad84a87..468438d0938 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1414,8 +1414,8 @@ module SpecialFloat =
let option_name = "-warn-special-float"
let default = "non-finite"
let arg_name = "none|nan|non-finite"
- let help = "generate alarms when special floats are produced: \
- infinite floats or NaN (by default), only on NaN or never."
+ let help = "generate alarms when special floats are produced: never, \
+ only on NaN, or on infinite floats and NaN (by default)."
end)
let () = SpecialFloat.set_possible_values ["none"; "nan"; "non-finite"]
--
GitLab