From 2e860e4d9ff4bbd9154c5f1751ebb98f3ace1d64 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 4 Jul 2019 14:47:28 +0200
Subject: [PATCH] [Kernel] -explain: do not fail on unknown options.
---
.../cmdline_parameters/cmdline.ml | 22 +++++++++++--------
1 file changed, 13 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 4b536083294..808046e9e91 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -1085,15 +1085,19 @@ let list_all_plugin_options ~print_invisible =
(* ************************************************************************* *)
let pp_option_help name =
- let option = Hashtbl.find Plugin.all_options name in
- let help =
- if option.oname = name then option.ohelp else
- "alias for " ^ option.oname ^ "\n" ^ option.ohelp
- in
- let argname = option.argname in
- let name = if argname = "" then name else name ^ " <" ^ argname ^ ">" in
- let print fmt = print_helpline fmt name help option.ext_help in
- Log.print_on_output print
+ try
+ let option = Hashtbl.find Plugin.all_options name in
+ let help =
+ if option.oname = name then option.ohelp else
+ "alias for " ^ option.oname ^ "\n" ^ option.ohelp
+ in
+ let argname = option.argname in
+ let name = if argname = "" then name else name ^ " <" ^ argname ^ ">" in
+ let print fmt = print_helpline fmt name help option.ext_help in
+ Log.print_on_output print
+ with Not_found ->
+ let print fmt = Format.fprintf fmt "Invalid option %s@." name in
+ Log.print_on_output print
(* [option_re] allows matching an option and extracting its name,
even when there is a '=', e.g. "-kernel-msg-key=-typing".
--
GitLab