From 5b6dd304b9f88c86ebb066c1f173bb011d2b5f83 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 30 Sep 2016 21:11:02 +0200 Subject: 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). --- library/goptions.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'library/goptions.mli') 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 -- cgit v1.2.3