diff options
| author | Gaëtan Gilbert | 2019-04-01 14:15:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-16 15:11:03 +0100 |
| commit | 1e1fd6d7e66cee0130a119bf1ded6b7dee17131c (patch) | |
| tree | dec256271cc14e401b358953867ba05e74fecae7 /library | |
| parent | 839ed4e80ca4dc068422c7c9fdb0c00e4ff1ebab (diff) | |
Command-line setters for options
TODO coqproject handling (for now it can be done through -arg I guess)
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.mli | 8 |
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; |
