From df3cbbee21cfaf03f7c2b9bd78280f25a5512f5a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 26 Jan 2021 13:24:25 +0100
Subject: [options] improve support for append

---
 stm/stm.ml  | 8 ++++++--
 stm/stm.mli | 5 ++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 1c06c1efb7..0b00524bd5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2305,7 +2305,10 @@ end (* }}} *)
 
 (** STM initialization options: *)
 
-type option_command = OptionSet of string option | OptionUnset
+type option_command =
+  | OptionSet of string option
+  | OptionAppend of string
+  | OptionUnset
 
 type injection_command =
   | OptionInjection of (Goptions.option_name * option_command)
@@ -2404,7 +2407,8 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
   let set_option = let open Goptions in function
       | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
       | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in
+      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
+      | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in
 
   let handle_injection = function
     | RequireInjection r -> require_file r
diff --git a/stm/stm.mli b/stm/stm.mli
index 097bcbe0ca..e0c33a309b 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,7 +52,10 @@ type stm_doc_type =
   | VioDoc      of string       (* file path *)
   | Interactive of interactive_top    (* module path *)
 
-type option_command = OptionSet of string option | OptionUnset
+type option_command =
+  | OptionSet of string option
+  | OptionAppend of string
+  | OptionUnset
 
 type injection_command =
   | OptionInjection of (Goptions.option_name * option_command)
-- 
cgit v1.2.3