From 0adac834aabcafd88835991025216c1b0bea7e72 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Sep 2020 13:50:42 +0200
Subject: [PATCH] [Kernel] remove obsolete and unused Cmdline.String_list
---
src/kernel_services/cmdline_parameters/cmdline.ml | 6 ------
src/kernel_services/cmdline_parameters/cmdline.mli | 1 -
2 files changed, 7 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 808046e9e91..7178eea308b 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -252,7 +252,6 @@ type option_setting =
| Unit of (unit -> unit)
| Int of (int -> unit)
| String of (string -> unit)
- | String_list of (string list -> unit)
exception Cannot_parse of string * string
let raise_error name because = raise (Cannot_parse(name, because))
@@ -310,10 +309,6 @@ let parse known_options_list then_expected options_list =
check_string_argname ();
f arg;
true
- | String_list f ->
- check_string_argname ();
- f (Str.split (Str.regexp "[ \t]*,[ \t]*") arg);
- true
in
unknown_options, use_arg && not explicit, true
with Not_found ->
@@ -896,7 +891,6 @@ let low_print_option_help fmt print_invisible o =
| Unit _ -> ""
| Int _ -> " <n>"
| String _ -> " <s>"
- | String_list _ -> " <s1, ..., sn>"
else
" <" ^ s ^ ">"
in
diff --git a/src/kernel_services/cmdline_parameters/cmdline.mli b/src/kernel_services/cmdline_parameters/cmdline.mli
index db33fb74584..b3eda2c34f9 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.mli
+++ b/src/kernel_services/cmdline_parameters/cmdline.mli
@@ -270,7 +270,6 @@ type option_setting =
| Unit of (unit -> unit)
| Int of (int -> unit)
| String of (string -> unit)
- | String_list of (string list -> unit)
val add_option:
string ->
--
GitLab