From 4f02ced607f23c340314b246b156ee70cd3a4f02 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 25 Aug 2020 09:59:33 +0200 Subject: [PATCH] [WP] fix exception raised by invalid option in -wp-why3-opt --- src/plugins/wp/Why3Provers.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml index 232c05888e6..ab50c9858b2 100644 --- a/src/plugins/wp/Why3Provers.ml +++ b/src/plugins/wp/Why3Provers.ml @@ -46,9 +46,9 @@ let configure = begin try Arg.parse_argv ~current:(ref 0) args (Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list]) - (fun _ -> raise (Arg.Help "Unknown why3 option")) + (fun opt -> raise (Arg.Bad ("unknown option: " ^ opt))) "Why3 options" - with Arg.Bad s -> Wp_parameters.abort "%s" s + with Arg.Bad s | Arg.Help s -> Wp_parameters.abort "%s" s end; ignore (Why3.Debug.Args.option_list ()); Why3.Debug.Args.set_flags_selected (); -- GitLab