diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-09-30 21:11:02 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-10-01 07:50:12 +0200 |
| commit | 5b6dd304b9f88c86ebb066c1f173bb011d2b5f83 (patch) | |
| tree | b1f30879412871ef7fdad8f23fc5de4e1dd0d0c8 /library/goptions.mli | |
| parent | 064de6f6839c4ef963b83018812c5d4113eb2bb9 (diff) | |
Allow appending to string options.
Whether an option should be set or appended to is stored as a 2-value
flag next to the new content. This commit also cleans the code by
declaring a single object for each persistent option rather than three
different ones (one per locality).
Diffstat (limited to 'library/goptions.mli')
| -rw-r--r-- | library/goptions.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/goptions.mli b/library/goptions.mli index 26864503b..ca2df0710 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -154,6 +154,7 @@ val get_ref_table : val set_int_option_value_gen : bool option -> option_name -> int option -> unit val set_bool_option_value_gen : bool option -> option_name -> bool -> unit val set_string_option_value_gen : bool option -> option_name -> string -> unit +val set_string_option_append_value_gen : bool option -> option_name -> string -> unit val unset_option_value_gen : bool option -> option_name -> unit val set_int_option_value : option_name -> int option -> unit |