From ae68452a9eddc0d1e49438df91adea4398b16b44 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 22 Feb 2019 11:47:22 +0100
Subject: [PATCH] [Kernel] fixes help message about -PLUGIN-warn-key
---
src/kernel_services/plugin_entry_points/plugin.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 6048de1b0a8..fa721f6e114 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -734,7 +734,7 @@ struct
let arg_name="k1[=s1][,...,kn[=sn]]"
let help =
"set warning status for category <k1> to <s1>,...,<kn> to <sn>. Use "
- ^ debug_category_optname
+ ^ warn_category_optname
^ " help to get a list of available categories, and * to enable \
all categories. Possible statuses are inactive, feedback-once, \
once, active, error-once, error, and abort. Defaults to active"
--
GitLab