aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-04-17 11:26:01 +0200
committerEmilio Jesus Gallego Arias2019-04-17 11:26:01 +0200
commit14a51bd079fb3ba5d2eece1dced219ce66702694 (patch)
treee5b8881bedc60a4e30a19842a965f1a2aaefaf3b /library
parent801c672defa3192cea522b5d8b34e5aef9fc37ee (diff)
parent1e1fd6d7e66cee0130a119bf1ded6b7dee17131c (diff)
Merge PR #9876: Command-line setters for options
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares
Diffstat (limited to 'library')
-rw-r--r--library/goptions.mli8
1 files changed, 8 insertions, 0 deletions
diff --git a/library/goptions.mli b/library/goptions.mli
index 9925eb9e7b..2e593e9d9e 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -172,6 +172,14 @@ type option_value =
| StringValue of string
| StringOptValue of string option
+val set_option_value : ?locality:option_locality ->
+ ('a -> option_value -> option_value) -> option_name -> 'a -> unit
+(** [set_option_value ?locality f name v] sets [name] to the result of
+ applying [f] to [v] and [name]'s current value. Use for behaviour
+ depending on the type of the option, eg erroring when ['a] doesn't
+ match it. Changing the type will result in errors later so don't do
+ that. *)
+
(** Summary of an option status *)
type option_state = {
opt_depr : bool;